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
rng phi = X by Th5;

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

thus (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal by A1; :: thesis: verum

end;

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

thus (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) . n is ordinal by A1; :: thesis: verum

end;

end;