let i be Instruction of SCM+FSA; :: thesis: for X being set st i in X holds

UsedIntLoc i c= UsedILoc X

let X be set ; :: thesis: ( i in X implies UsedIntLoc i c= UsedILoc X )

assume A1: i in X ; :: thesis: UsedIntLoc i c= UsedILoc X

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedIntLoc i or e in UsedILoc X )

assume A2: e in UsedIntLoc i ; :: thesis: e in UsedILoc X

UsedIntLoc i in { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in X } by A1;

hence e in UsedILoc X by A2, TARSKI:def 4; :: thesis: verum

UsedIntLoc i c= UsedILoc X

let X be set ; :: thesis: ( i in X implies UsedIntLoc i c= UsedILoc X )

assume A1: i in X ; :: thesis: UsedIntLoc i c= UsedILoc X

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedIntLoc i or e in UsedILoc X )

assume A2: e in UsedIntLoc i ; :: thesis: e in UsedILoc X

UsedIntLoc i in { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in X } by A1;

hence e in UsedILoc X by A2, TARSKI:def 4; :: thesis: verum