X c= NAT by ORDINAL1:def 12;
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 Th5;

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

phi . n in rng phi by A3, FUNCT_1:def 3;
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 2; :: thesis: verum

end;

end;