let i be Instruction of SCM+FSA; :: thesis: for X being set st i in X holds
UsedInt*Loc i c= UsedI*Loc X
let X be set ; :: thesis: ( i in X implies UsedInt*Loc i c= UsedI*Loc X )
assume A1: i in X ; :: thesis: UsedInt*Loc i c= UsedI*Loc X
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedInt*Loc i or e in UsedI*Loc X )
assume A2: e in UsedInt*Loc i ; :: thesis: e in UsedI*Loc X
UsedInt*Loc i in { (UsedInt*Loc j) where j is Instruction of SCM+FSA : j in X } by A1;
hence e in UsedI*Loc X by A2, TARSKI:def 4; :: thesis: verum