let n be Element of 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 A1: x in { l where l is Element of NAT : l < n } ; :: thesis: x in NAT
ex l being Element of NAT st
( x = l & l < n ) by A1;
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:30; :: thesis: verum