consider phi being Ordinal-Sequence such that
A1: ( phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) & phi is increasing & 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 n in dom phi ; :: thesis: (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . n is ordinal

then phi . n in rng phi by FUNCT_1:def 5;
hence (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . n is ordinal 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 ordinal

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

end;

end;