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

proof

hence
{ (IC (Exec (i,ss))) where ss is Element of product (the_Values_of S) : IC ss = l } is Subset of NAT
; :: thesis: verum
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;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