let A be Ordinal; :: thesis:
set M = card A;
card A,A are_equipotent by CARD_1:def 5;
then consider f being Function such that
A1: ( f is one-to-one & dom f = card A & rng f = A ) by WELLORD2:def 4;
defpred S₁[ set ] means not f . $1 in Union (f | $1);
consider X being set such that
A2: for x being set holds
( x in X iff ( x in card A & S₁[x] ) ) from XBOOLE_0:sch 1();
reconsider f = f as T-Sequence by A1, ORDINAL1:def 7;
reconsider f = f as Ordinal-Sequence by A1, ORDINAL2:def 8;
set R = RelIncl X;
set B = order_type_of (RelIncl X);
set phi = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X);
take order_type_of (RelIncl X) ; :: thesis:
A3: X c= card A

let x be set ; :: according to TARSKI:def 3 :: thesis:
thus ( not x in X or x in card A ) by A2; :: thesis:

end;

proof

let a, b be Ordinal; :: according to ORDINAL2:def 16 :: thesis:
assume A8: ( a in b & b in dom xi ) ; :: thesis:
then A9: ( a in dom xi & a c= b & a <> b & xi is one-to-one ) by A1, A6, ORDINAL1:19, ORDINAL1:def 2;
then A10: ( phi . a <> phi . b & [a,b] in RelIncl (order_type_of (RelIncl X)) & phi . a in X & phi . b in X ) by A6, A7, A8, FUNCT_1:def 5, FUNCT_1:def 8, WELLORD2:def 1;
reconsider a' = phi . a, b' = phi . b as Ordinal ;
reconsider a'' = f . a', b'' = f . b' as Ordinal ;
[(phi . a),(phi . b)] in RelIncl X by A5, A10, WELLORD1:def 7;
then a' c= b' by A10, WELLORD2:def 1;
then a' c< b' by A10, XBOOLE_0:def 8;
then A11: ( a' in b' & not b'' in Union (f | b') & a'' <> b'' ) by A1, A2, A3, A10, FUNCT_1:def 8, ORDINAL1:21;
then ( a'' in rng (f | b') & Union (f | b') = union (rng (f | b')) ) by A1, A3, A10, FUNCT_1:73;
then ( a'' c= Union (f | b') & Union (f | b') c= b'' ) by A11, ORDINAL1:26, ZFMISC_1:92;
then A12: ( a'' c= b'' & a'' = xi . a & b'' = xi . b ) by A8, A9, FUNCT_1:22, XBOOLE_1:1;
then a'' c< b'' by A11, XBOOLE_0:def 8;
hence xi . a in xi . b by A12, ORDINAL1:21; :: thesis:

end;

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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
then consider y being set such that
A14: ( y in dom f & x = f . y ) by A1, FUNCT_1:def 5;
reconsider x' = x, y = y as Ordinal by A14;

per cases ;

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

then y in X by A1, A2, A14;
then consider z being set such that
A15: ( z in order_type_of (RelIncl X) & y = phi . z ) by A6, FUNCT_1:def 5;
( x' = xi . z & xi . z in rng xi ) by A7, A14, A15, FUNCT_1:22, FUNCT_1:def 5;
hence x in sup xi by ORDINAL2:27; :: thesis:

end;

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

then consider z being set such that
A16: ( z in dom (f | y) & f . y in (f | y) . z ) by Th10;
reconsider z = z as Ordinal by A16;
defpred S₂[ Ordinal] means ( $1 in y & f . y in f . $1 );
dom (f | y) = (dom f) /\ y by RELAT_1:90;
then ( (f | y) . z = f . z & z in y ) by A16, FUNCT_1:70, XBOOLE_0:def 4;
then A17: ex C being Ordinal st S₂[C] by A16;
consider C being Ordinal such that
A18: ( S₂[C] & ( for B being Ordinal st S₂[B] holds
C c= B ) ) from ORDINAL1:sch 1(A17);

thus C in card A by A1, A14, A18, ORDINAL1:19; :: thesis:
assume f . C in Union (f | C) ; :: thesis:
then consider a being set such that
A19: ( a in dom (f | C) & f . C in (f | C) . a ) by Th10;
reconsider a = a as Ordinal by A19;
reconsider fa = (f | C) . a, fc = f . C, fy = f . y as Ordinal ;
( dom (f | C) = (dom f) /\ C & f . a = fa & fc in fa ) by A19, FUNCT_1:70, RELAT_1:90;
then A20: ( a in C & fy in f . a ) by A18, A19, ORDINAL1:19, XBOOLE_0:def 4;
then ( a in y & not C c= a ) by A18, ORDINAL1:7, ORDINAL1:19;
hence contradiction by A18, A20; :: thesis:

end;

then C in X by A2;
then consider z being set such that
A21: ( z in order_type_of (RelIncl X) & C = phi . z ) by A6, FUNCT_1:def 5;
reconsider z = z as Ordinal by A21;
reconsider xz = xi . z as Ordinal ;
( xz = f . C & xz in rng xi ) by A7, A21, FUNCT_1:22, FUNCT_1:def 5;
then ( xz in sup xi & x' in xz ) by A14, A18, ORDINAL2:27;
hence x in sup xi by ORDINAL1:19; :: thesis:

end;

hence x in sup xi ; :: thesis:

end;

sup A = A by ORDINAL2:26;
hence sup xi c= A by A7, ORDINAL2:30; :: thesis: