let A be Ordinal; :: thesis: for X being set st X c= A holds
ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
let X be set ; :: thesis: ( X c= A implies ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X ) )
set R = RelIncl X;
set B = order_type_of (RelIncl X);
set phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X);
assume A1: X c= A ; :: thesis: ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
then A2: ( RelIncl X is well-ordering & RelIncl (order_type_of (RelIncl X)) is well-ordering & order_type_of (RelIncl X) c= A ) by WELLORD2:9, WELLORD2:17;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def 2;
then RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic by WELLORD1:50;
then A3: ( canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X & field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) & field (RelIncl X) = X ) by A2, WELLORD1:def 9, WELLORD2:def 1;
then A4: ( dom (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) = order_type_of (RelIncl X) & rng (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) = X & canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) is one-to-one & ( for x, y being set holds
( [x,y] in RelIncl (order_type_of (RelIncl X)) iff ( x in order_type_of (RelIncl X) & y in order_type_of (RelIncl X) & [((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . x),((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . y)] in RelIncl X ) ) ) ) by WELLORD1:def 7;
then reconsider phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) as T-Sequence by ORDINAL1:def 7;
reconsider phi = phi as Ordinal-Sequence by A1, A4, ORDINAL2:def 8;
take phi ; :: thesis: ( phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) & phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
thus phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) ; :: thesis: ( phi is increasing & dom phi = order_type_of (RelIncl X) & rng phi = X )
thus phi is increasing :: thesis: ( dom phi = order_type_of (RelIncl X) & rng phi = X )

proof

let a, b be Ordinal; :: according to ORDINAL2:def 16 :: thesis: ( not a in b or not b in dom phi or phi . a in phi . b )
assume A5: ( a in b & b in dom phi ) ; :: thesis: phi . a in phi . b
then A6: ( a in dom phi & a c= b & a <> b ) by ORDINAL1:19, ORDINAL1:def 2;
reconsider a' = phi . a, b' = phi . b as Ordinal ;
[a,b] in RelIncl (order_type_of (RelIncl X)) by A4, A5, A6, WELLORD2:def 1;
then ( [a',b'] in RelIncl X & a' in X & b' in X ) by A4, A5, A6, FUNCT_1:def 5;
then ( a' c= b' & a' <> b' ) by A4, A5, A6, FUNCT_1:def 8, WELLORD2:def 1;
then ( a' c< b' & a' <> b' ) by XBOOLE_0:def 8;
hence phi . a in phi . b by ORDINAL1:21; :: thesis: verum

end;

thus ( dom phi = order_type_of (RelIncl X) & rng phi = X ) by A3, WELLORD1:def 7; :: thesis: verum