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

hence n is Subset of NAT by AXIOMS:4; :: thesis: verum

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

x in NAT

then
{ l where l is Nat : l < n } c= NAT
;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;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

hence n is Subset of NAT by AXIOMS:4; :: thesis: verum