let X, Y be set ; :: thesis: ( X c= Y implies UsedI*Loc X c= UsedI*Loc Y )

assume A1: X c= Y ; :: thesis: UsedI*Loc X c= UsedI*Loc Y

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedI*Loc X or e in UsedI*Loc Y )

assume e in UsedI*Loc X ; :: thesis: e in UsedI*Loc Y

then consider B being set such that

A2: e in B and

A3: B in { (UsedInt*Loc 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 = UsedInt*Loc i and

A5: i in X by A3;

i in Y by A1, A5;

then B in { (UsedInt*Loc j) where j is Instruction of SCM+FSA : j in Y } by A4;

hence e in UsedI*Loc Y by A2, TARSKI:def 4; :: thesis: verum

assume A1: X c= Y ; :: thesis: UsedI*Loc X c= UsedI*Loc Y

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in UsedI*Loc X or e in UsedI*Loc Y )

assume e in UsedI*Loc X ; :: thesis: e in UsedI*Loc Y

then consider B being set such that

A2: e in B and

A3: B in { (UsedInt*Loc 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 = UsedInt*Loc i and

A5: i in X by A3;

i in Y by A1, A5;

then B in { (UsedInt*Loc j) where j is Instruction of SCM+FSA : j in Y } by A4;

hence e in UsedI*Loc Y by A2, TARSKI:def 4; :: thesis: verum