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

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