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;