{ (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } c= NAT

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } or e in NAT )
assume e in { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } ; :: thesis: e in NAT
then ex ss being Element of product (the_Values_of S) st
( e = IC (Exec (i,ss)) & IC ss = l ) ;
hence e in NAT ; :: thesis: verum

end;

hence { (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } is Subset of NAT ; :: thesis: verum