consider x being Element of X;
A1: X \ {x}, card (X \ {x}) are_equipotent by CARD_1:def 5;
A2: {x},{(card (X \ {x}))} are_equipotent by CARD_1:48;
A3: {x} misses X \ {x} by XBOOLE_1:79;
not card (X \ {x}) in card (X \ {x}) ;
then A4: {(card (X \ {x}))} misses card (X \ {x}) by ZFMISC_1:56;
A5: ( succ (card (X \ {x})) = (card (X \ {x})) \/ {(card (X \ {x}))} & X = (X \ {x}) \/ {x} ) by Lm1, ORDINAL1:def 1;
then X, succ (card (X \ {x})) are_equipotent by A1, A2, A3, A4, CARD_1:58;
then consider r being Order of X such that
A6: r well_orders X and
A7: order_type_of r = succ (card (X \ {x})) by Th7;
A8: field r = X by ORDERS_1:100;
then r is well-ordering by A6, 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
A9: f is_isomorphism_of RelIncl (order_type_of r),r by WELLORD1:def 8;
field (RelIncl (order_type_of r)) = order_type_of r by WELLORD2:def 1;
then A10: ( f is one-to-one & dom f = order_type_of r & rng f = X ) by A8, A9, WELLORD1:def 7;
take r ; :: thesis: ( r is upper-bounded & r is well-ordering )
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 )
assume A11: y in field r ; :: thesis: [y,a] in r
then A12: (f " ) . y in order_type_of r by A8, A10, FUNCT_1:54;
then A13: ( (f " ) . y in card (X \ {x}) or (f " ) . y = card (X \ {x}) ) by A5, A7, SETWISEO:6;
reconsider b = (f " ) . y as Ordinal by A12;
( b c= card (X \ {x}) & card (X \ {x}) in order_type_of r ) by A5, A7, A13, ORDINAL1:def 2, SETWISEO:6;
then [b,(card (X \ {x}))] in RelIncl (order_type_of r) by A12, WELLORD2:def 1;
then [(f . b),a] in r by A9, WELLORD1:def 7;
hence [y,a] in r by A8, A10, A11, FUNCT_1:57; :: thesis: verum

end;

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