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

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 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;

thus r is well-ordering by A4, A6, WELLORD1:4; :: thesis: verum