let n be Nat; :: thesis: n is Subset of NAT

now

let x be set ; :: thesis: ( x in { l where l is Element of NAT : l < n } implies x in NAT )
assume x in { l where l is Element of NAT : l < n } ; :: thesis: x in NAT
then ex l being Element of NAT st
( x = l & l < n ) ;
hence x in NAT ; :: thesis: verum

end;

then { l where l is Element of NAT : l < n } c= NAT by TARSKI:def 3;
hence n is Subset of NAT by AXIOMS:4; :: thesis: verum