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
; ( 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
r is well-ordering proof
take a =
f . (card (X \ { the Element of X}));
YELLOW21:def 9 for y being set st y in field r holds
[y,a] in r
let y be
set ;
( 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
;
[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;
verum
end;
thus
r is well-ordering
by A4, A6, WELLORD1:4; verum