X c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in NAT )
assume x in X ; :: thesis: x in NAT
hence x in NAT by ORDINAL1:def 13; :: thesis: verum

end;

then reconsider X = X as Subset of NAT ;
consider phi being Ordinal-Sequence such that
A1: phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) and
phi is increasing and
dom phi = order_type_of (RelIncl X) and
A2: rng phi = X by CARD_5:14;

per cases ( n in dom phi or not n in dom phi ) ;

suppose A3: n in dom phi ; :: thesis: (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . n is natural

then reconsider a = phi . n as Element of X by A2, FUNCT_1:def 5;
phi . n in rng phi by A3, FUNCT_1:def 5;
hence (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . n is natural by A1, A2; :: thesis: verum

end;

suppose not n in dom phi ; :: thesis: (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . n is natural

hence (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . n is natural by A1, FUNCT_1:def 4; :: thesis: verum

end;

end;