let x be Surreal; ( not R_ x is empty & R_ x is finite & x is uSurreal implies card (R_ x) = 1 )
assume A1:
( not R_ x is empty & R_ x is finite & x is uSurreal )
; card (R_ x) = 1
then consider Min, Max being Surreal such that
A2:
( Min in R_ x & Max in R_ x )
and
A3:
for y being Surreal st y in R_ x holds
( Min <= y & y <= Max )
by Th12;
reconsider c = card (R_ x) as Nat by A1;
assume A4:
card (R_ x) <> 1
; contradiction
set B = born_eq x;
x = Unique_No x
by Def11, A1;
then A5:
x in (unique_No_op (born_eq x)) . (born_eq x)
by Def10;
A6:
born_eq x in succ (born_eq x)
by ORDINAL1:6;
A7:
born_eq x = born x
by A5, Th38;
then
not x in union (rng ((unique_No_op (born_eq x)) | (born_eq x)))
by A5, Th38;
then consider Y being non empty surreal-membered set such that
A8:
( Y = (born_eq_set x) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & x = the Y -smallest Surreal )
by A5, A6, Def9;
A9:
for y being Surreal st y in R_ x holds
Min <= y
by A3;
then reconsider Mx = [(L_ x),{Min}] as Surreal by A2, Th24;
A10:
( Mx == x & born Mx c= born x )
by A9, A2, Th24;
x in Y
by A8, Def7;
then
x in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))
by A8, XBOOLE_0:def 4;
then A11:
(L_ x) \/ (R_ x) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x)))
by Def8;
(L_ Mx) \/ (R_ Mx) c= (L_ x) \/ (R_ x)
by XBOOLE_1:9, A2, ZFMISC_1:31;
then
(L_ Mx) \/ (R_ Mx) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x)))
by A11, XBOOLE_1:1;
then A12:
Mx in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))
by Def8;
( Mx in Day (born Mx) & Day (born Mx) c= Day (born x) )
by A9, A2, Th24, SURREAL0:def 18, SURREAL0:35;
then
Mx in born_eq_set x
by A7, A10, Def6;
then
Mx in Y
by A8, A12, XBOOLE_0:def 4;
then A13:
(card (L_ x)) (+) (card (R_ x)) c= (card (L_ Mx)) (+) (card (R_ Mx))
by A10, A8, Def7;
A14:
card (R_ Mx) = 1
by CARD_1:30;
1 in Segm c
by A4, A1, NAT_1:25, NAT_1:44;
then
(card (L_ Mx)) (+) (card (R_ Mx)) in (card (L_ x)) (+) (card (R_ x))
by A14, ORDINAL7:94;
hence
contradiction
by A13, ORDINAL1:12; verum