set x = the Element of X;

A1: ( X \ { the Element of X}, card (X \ { the Element of X}) are_equipotent & { the Element of X},{(card (X \ { the Element of X}))} are_equipotent ) by CARD_1:28, CARD_1:def 2;

A2: succ (card (X \ { the Element of X})) = (card (X \ { the Element of X})) \/ {(card (X \ { the Element of X}))} by ORDINAL1:def 1;

not card (X \ { the Element of X}) in card (X \ { the Element of X}) ;

then A3: {(card (X \ { the Element of X}))} misses card (X \ { the Element of X}) by ZFMISC_1:50;

( { the Element of X} misses X \ { the Element of X} & X = (X \ { the Element of X}) \/ { the Element of X} ) by Lm1, XBOOLE_1:79;

then consider r being Order of X such that

A4: r well_orders X and

A5: order_type_of r = succ (card (X \ { the Element of X})) by A1, A3, A2, Th7, CARD_1:31;

take r ; :: thesis: ( r is upper-bounded & r is well-ordering )

A6: field r = X by ORDERS_1:15;

then r is well-ordering by A4, WELLORD1:4;

then r, RelIncl (order_type_of r) are_isomorphic by WELLORD2:def 2;

then RelIncl (order_type_of r),r are_isomorphic by WELLORD1:40;

then consider f being Function such that

A7: f is_isomorphism_of RelIncl (order_type_of r),r ;

A8: f is one-to-one by A7;

A9: rng f = X by A6, A7;

field (RelIncl (order_type_of r)) = order_type_of r by WELLORD2:def 1;

then A10: dom f = order_type_of r by A7;

thus r is upper-bounded :: thesis: r is well-ordering

A1: ( X \ { the Element of X}, card (X \ { the Element of X}) are_equipotent & { the Element of X},{(card (X \ { the Element of X}))} are_equipotent ) by CARD_1:28, CARD_1:def 2;

A2: succ (card (X \ { the Element of X})) = (card (X \ { the Element of X})) \/ {(card (X \ { the Element of X}))} by ORDINAL1:def 1;

not card (X \ { the Element of X}) in card (X \ { the Element of X}) ;

then A3: {(card (X \ { the Element of X}))} misses card (X \ { the Element of X}) by ZFMISC_1:50;

( { the Element of X} misses X \ { the Element of X} & X = (X \ { the Element of X}) \/ { the Element of X} ) by Lm1, XBOOLE_1:79;

then consider r being Order of X such that

A4: r well_orders X and

A5: order_type_of r = succ (card (X \ { the Element of X})) by A1, A3, A2, Th7, CARD_1:31;

take r ; :: thesis: ( r is upper-bounded & r is well-ordering )

A6: field r = X by ORDERS_1:15;

then r is well-ordering by A4, WELLORD1:4;

then r, RelIncl (order_type_of r) are_isomorphic by WELLORD2:def 2;

then RelIncl (order_type_of r),r are_isomorphic by WELLORD1:40;

then consider f being Function such that

A7: f is_isomorphism_of RelIncl (order_type_of r),r ;

A8: f is one-to-one by A7;

A9: rng f = X by A6, A7;

field (RelIncl (order_type_of r)) = order_type_of r by WELLORD2:def 1;

then A10: dom f = order_type_of r by A7;

thus r is upper-bounded :: thesis: r is well-ordering

proof

thus
r is well-ordering
by A4, A6, WELLORD1:4; :: thesis: verum
take a = f . (card (X \ { the Element of X})); :: according to YELLOW21:def 9 :: thesis: for y being set st y in field r holds

[y,a] in r

let y be set ; :: thesis: ( y in field r implies [y,a] in r )

A11: card (X \ { the Element of X}) in order_type_of r by A2, A5, ZFMISC_1:136;

assume A12: y in field r ; :: thesis: [y,a] in r

then A13: (f ") . y in order_type_of r by A6, A8, A10, A9, FUNCT_1:32;

then reconsider b = (f ") . y as Ordinal ;

( (f ") . y in card (X \ { the Element of X}) or (f ") . y = card (X \ { the Element of X}) ) by A2, A5, A13, ZFMISC_1:136;

then b c= card (X \ { the Element of X}) by ORDINAL1:def 2;

then [b,(card (X \ { the Element of X}))] in RelIncl (order_type_of r) by A13, A11, WELLORD2:def 1;

then [(f . b),a] in r by A7;

hence [y,a] in r by A6, A8, A9, A12, FUNCT_1:35; :: thesis: verum

end;[y,a] in r

let y be set ; :: thesis: ( y in field r implies [y,a] in r )

A11: card (X \ { the Element of X}) in order_type_of r by A2, A5, ZFMISC_1:136;

assume A12: y in field r ; :: thesis: [y,a] in r

then A13: (f ") . y in order_type_of r by A6, A8, A10, A9, FUNCT_1:32;

then reconsider b = (f ") . y as Ordinal ;

( (f ") . y in card (X \ { the Element of X}) or (f ") . y = card (X \ { the Element of X}) ) by A2, A5, A13, ZFMISC_1:136;

then b c= card (X \ { the Element of X}) by ORDINAL1:def 2;

then [b,(card (X \ { the Element of X}))] in RelIncl (order_type_of r) by A13, A11, WELLORD2:def 1;

then [(f . b),a] in r by A7;

hence [y,a] in r by A6, A8, A9, A12, FUNCT_1:35; :: thesis: verum