consider x being Element of X;
A1: ( X \ {x}, card (X \ {x}) are_equipotent & {x},{(card (X \ {x}))} are_equipotent ) by CARD_1:48, CARD_1:def 5;
A2: succ (card (X \ {x})) = (card (X \ {x})) \/ {(card (X \ {x}))} by ORDINAL1:def 1;
not card (X \ {x}) in card (X \ {x}) ;
then A3: {(card (X \ {x}))} misses card (X \ {x}) by ZFMISC_1:56;
( {x} misses X \ {x} & X = (X \ {x}) \/ {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 \ {x})) by A1, A3, A2, Th7, CARD_1:58;
take r ; :: thesis: ( r is upper-bounded & r is well-ordering )
A6: field r = X by ORDERS_1:100;
then r is well-ordering by A4, WELLORD1:8;
then r, RelIncl (order_type_of r) are_isomorphic by WELLORD2:def 2;
then RelIncl (order_type_of r),r are_isomorphic by WELLORD1:50;
then consider f being Function such that
A7: f is_isomorphism_of RelIncl (order_type_of r),r by WELLORD1:def 8;
A8: f is one-to-one by A7, WELLORD1:def 7;
A9: rng f = X by A6, A7, WELLORD1:def 7;
field (RelIncl (order_type_of r)) = order_type_of r by WELLORD2:def 1;
then A10: dom f = order_type_of r by A7, WELLORD1:def 7;
thus r is upper-bounded :: thesis: r is well-ordering

proof

take a = f . (card (X \ {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 \ {x}) in order_type_of r by A2, A5, SETWISEO:6;
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:54;
then reconsider b = (f " ) . y as Ordinal ;
( (f " ) . y in card (X \ {x}) or (f " ) . y = card (X \ {x}) ) by A2, A5, A13, SETWISEO:6;
then b c= card (X \ {x}) by ORDINAL1:def 2;
then [b,(card (X \ {x}))] in RelIncl (order_type_of r) by A13, A11, WELLORD2:def 1;
then [(f . b),a] in r by A7, WELLORD1:def 7;
hence [y,a] in r by A6, A8, A9, A12, FUNCT_1:57; :: thesis: verum

end;

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