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

now :: thesis: for x being object st x in { l where l is Nat : l < n } holds
x in NAT

let x be object ; :: thesis: ( x in { l where l is Nat : l < n } implies x in NAT )
assume x in { l where l is Nat : l < n } ; :: thesis: x in NAT
then ex l being Nat st
( x = l & l < n ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

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