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 ;
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 ;
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 ;
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 ;
then r, RelIncl () are_isomorphic by WELLORD2:def 2;
then RelIncl (),r are_isomorphic by WELLORD1:40;
then consider f being Function such that
A7: f is_isomorphism_of RelIncl (),r ;
A8: f is one-to-one by A7;
A9: rng f = X by A6, A7;
field () = order_type_of r by WELLORD2:def 1;
then A10: dom f = order_type_of r by A7;
thus r is upper-bounded :: thesis:
proof
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 ;
assume A12: y in field r ; :: thesis: [y,a] in r
then A13: (f ") . y in order_type_of r by ;
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 ;
then b c= card (X \ { the Element of X}) by ORDINAL1:def 2;
then [b,(card (X \ { the Element of X}))] in RelIncl () by ;
then [(f . b),a] in r by A7;
hence [y,a] in r by ; :: thesis: verum
end;
thus r is well-ordering by ; :: thesis: verum