let X, Y be set ; :: thesis: ( X c= Y implies UsedILoc X c= UsedILoc Y )
assume A1: X c= Y ; :: thesis: UsedILoc X c= UsedILoc Y
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedILoc X or e in UsedILoc Y )
assume e in UsedILoc X ; :: thesis: e in UsedILoc Y
then consider B being set such that
A2: e in B and
A3: B in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } by TARSKI:def 4;
consider i being Instruction of SCM+FSA such that
A4: B = UsedIntLoc i and
A5: i in X by A3;
i in Y by A1, A5;
then B in { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in Y } by A4;
hence e in UsedILoc Y by A2, TARSKI:def 4; :: thesis: verum