set A = { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } ;

union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } c= Int-Locations

union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } c= Int-Locations

proof

hence
union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } is Subset of Int-Locations
; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } or e in Int-Locations )

assume e in union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } ; :: thesis: e in Int-Locations

then consider B being set such that

A1: e in B and

A2: B in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } by TARSKI:def 4;

ex i being Instruction of SCM+FSA st

( B = UsedIntLoc i & i in X ) by A2;

then B c= Int-Locations by FINSUB_1:def 5;

hence e in Int-Locations by A1; :: thesis: verum

end;assume e in union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } ; :: thesis: e in Int-Locations

then consider B being set such that

A1: e in B and

A2: B in { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } by TARSKI:def 4;

ex i being Instruction of SCM+FSA st

( B = UsedIntLoc i & i in X ) by A2;

then B c= Int-Locations by FINSUB_1:def 5;

hence e in Int-Locations by A1; :: thesis: verum