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