let A be Ordinal; :: thesis:
set M = card A;
card A,A are_equipotent by CARD_1:def 2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = card A and
A3: rng f = A by WELLORD2:def 4;
defpred S₁[ set ] means not f . $1 in Union (f | $1);
reconsider f = f as Sequence by A2, ORDINAL1:def 7;
reconsider f = f as Ordinal-Sequence by A3, ORDINAL2:def 4;
consider X being set such that
A4: for x being set holds
( x in X iff ( x in card A & S₁[x] ) ) from XFAMILY:sch 1();
set R = RelIncl X;
set B = order_type_of (RelIncl X);
take order_type_of (RelIncl X) ; :: thesis:
A5: X c= card A by A4;
hence order_type_of (RelIncl X) c= card A by WELLORD2:14; :: thesis:
set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X));
RelIncl X is well-ordering by A5, WELLORD2:8;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def 2;
then ( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic ) by WELLORD1:40, WELLORD2:8;
then A6: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X by WELLORD1:def 9;
then A7: canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one by WELLORD1:def 7;
field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) by WELLORD2:def 1;
then A8: dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X) by A6, WELLORD1:def 7;
field (RelIncl X) = X by WELLORD2:def 1;
then A9: rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X by A6, WELLORD1:def 7;
reconsider phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) as Sequence by A8, ORDINAL1:def 7;
reconsider phi = phi as Ordinal-Sequence by A5, A9, ORDINAL2:def 4;
A10: dom (f * phi) = order_type_of (RelIncl X) by A2, A5, A8, A9, RELAT_1:27;
then reconsider xi = f * phi as Sequence by ORDINAL1:def 7;
rng (f * phi) c= A by A3, RELAT_1:26;
then reconsider xi = xi as Ordinal-Sequence by ORDINAL2:def 4;
take xi ; :: according to ORDINAL2:def 17 :: thesis:
thus ( dom xi = order_type_of (RelIncl X) & rng xi c= A ) by A2, A3, A5, A8, A9, RELAT_1:26, RELAT_1:27; :: thesis:
thus xi is increasing :: thesis:

proof

let a, b be Ordinal; :: according to ORDINAL2:def 12 :: thesis:
assume that
A11: a in b and
A12: b in dom xi ; :: thesis:
A13: a in dom xi by A11, A12, ORDINAL1:10;
then A14: phi . a in X by A8, A9, A10, FUNCT_1:def 3;
a <> b by A11;
then A15: phi . a <> phi . b by A8, A7, A10, A12, A13;
reconsider a9 = phi . a, b9 = phi . b as Ordinal ;
reconsider a99 = f . a9, b99 = f . b9 as Ordinal ;
A16: phi . b in X by A8, A9, A10, A12, FUNCT_1:def 3;
then not b99 in Union (f | b9) by A4;
then A17: Union (f | b9) c= b99 by ORDINAL1:16;
a c= b by A11, ORDINAL1:def 2;
then [a,b] in RelIncl (order_type_of (RelIncl X)) by A10, A12, A13, WELLORD2:def 1;
then [(phi . a),(phi . b)] in RelIncl X by A6, WELLORD1:def 7;
then a9 c= b9 by A14, A16, WELLORD2:def 1;
then a9 c< b9 by A15;
then a9 in b9 by ORDINAL1:11;
then a99 c= Union (f | b9) by A2, A5, A14, FUNCT_1:50, ZFMISC_1:74;
then A18: a99 c= b99 by A17;
a99 <> b99 by A1, A2, A5, A15, A14, A16;
then A19: a99 c< b99 by A18;
( a99 = xi . a & b99 = xi . b ) by A11, A12, FUNCT_1:12, ORDINAL1:10;
hence xi . a in xi . b by A19, ORDINAL1:11; :: thesis:

end;

thus A c= sup xi :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis:
assume x in A ; :: thesis:
then consider y being object such that
A20: y in dom f and
A21: x = f . y by A3, FUNCT_1:def 3;
reconsider x9 = x, y = y as Ordinal by A20;

now :: thesis:

per cases ;

suppose not f . y in Union (f | y) ; :: thesis:

then y in X by A2, A4, A20;
then consider z being object such that
A22: ( z in order_type_of (RelIncl X) & y = phi . z ) by A8, A9, FUNCT_1:def 3;
( x9 = xi . z & xi . z in rng xi ) by A10, A21, A22, FUNCT_1:12, FUNCT_1:def 3;
hence x in sup xi by ORDINAL2:19; :: thesis:

end;

suppose A23: f . y in Union (f | y) ; :: thesis:

defpred S₂[ Ordinal] means ( $1 in y & f . y in f . $1 );
consider z being object such that
A24: z in dom (f | y) and
A25: f . y in (f | y) . z by A23, Th2;
reconsider z = z as Ordinal by A24;
A26: (f | y) . z = f . z by A24, FUNCT_1:47;
dom (f | y) = (dom f) /\ y by RELAT_1:61;
then z in y by A24, XBOOLE_0:def 4;
then A27: ex C being Ordinal st S₂[C] by A25, A26;
consider C being Ordinal such that
A28: ( S₂[C] & ( for B being Ordinal st S₂[B] holds
C c= B ) ) from ORDINAL1:sch 1(A27);

now :: thesis:

thus C in card A by A2, A20, A28, ORDINAL1:10; :: thesis:
assume f . C in Union (f | C) ; :: thesis:
then consider a being object such that
A29: a in dom (f | C) and
A30: f . C in (f | C) . a by Th2;
reconsider a = a as Ordinal by A29;
reconsider fa = (f | C) . a, fy = f . y as Ordinal ;
f . a = fa by A29, FUNCT_1:47;
then A31: fy in f . a by A28, A30, ORDINAL1:10;
dom (f | C) = (dom f) /\ C by RELAT_1:61;
then A32: a in C by A29, XBOOLE_0:def 4;
then a in y by A28, ORDINAL1:10;
hence contradiction by A28, A32, A31, ORDINAL1:5; :: thesis:

end;

then C in X by A4;
then consider z being object such that
A33: z in order_type_of (RelIncl X) and
A34: C = phi . z by A8, A9, FUNCT_1:def 3;
reconsider z = z as Ordinal by A33;
reconsider xz = xi . z as Ordinal ;
xz in rng xi by A10, A33, FUNCT_1:def 3;
then A35: xz in sup xi by ORDINAL2:19;
x9 in xz by A10, A21, A28, A33, A34, FUNCT_1:12;
hence x in sup xi by A35, ORDINAL1:10; :: thesis:

end;

end;

end;

hence x in sup xi ; :: thesis:

end;

sup A = A by ORDINAL2:18;
hence sup xi c= A by A3, ORDINAL2:22, RELAT_1:26; :: thesis: