let A be Ordinal; :: thesis: No_uOrdinal_op (succ A) = [{(No_uOrdinal_op A)},{}]
set OA = No_uOrdinal_op A;
set x = [{(No_uOrdinal_op A)},{}];
A1: {(No_uOrdinal_op A)} << {} ;
A2: born (No_uOrdinal_op A) = A by Th73;
then A3: No_uOrdinal_op A in Day A by SURREAL0:def 18;
for o being object st o in {(No_uOrdinal_op A)} \/ {} holds
ex O being Ordinal st
( O in succ A & o in Day O )

proof

let o be object ; :: thesis: ( o in {(No_uOrdinal_op A)} \/ {} implies ex O being Ordinal st
( O in succ A & o in Day O ) )
assume o in {(No_uOrdinal_op A)} \/ {} ; :: thesis: ex O being Ordinal st
( O in succ A & o in Day O )
then o = No_uOrdinal_op A by TARSKI:def 1;
hence ex O being Ordinal st
( O in succ A & o in Day O ) by A3, ORDINAL1:6; :: thesis: verum

end;

then A4: [{(No_uOrdinal_op A)},{}] in Day (succ A) by A1, SURREAL0:46;
then reconsider x = [{(No_uOrdinal_op A)},{}] as Surreal ;
A5: No_Ordinal_op (succ A) = [{(No_Ordinal_op A)},{}] by Th65;
No_uOrdinal_op A == No_Ordinal_op A by Th73;
then {(No_uOrdinal_op A)} <==> {(No_Ordinal_op A)} by SURREALO:32;
then A6: x == No_Ordinal_op (succ A) by A5, SURREALO:29;
A7: born x c= succ A by A4, SURREAL0:def 18;
No_uOrdinal_op A in (L_ x) \/ (R_ x) by TARSKI:def 1;
then A8: succ A c= born x by A2, SURREALO:1, ORDINAL1:21;
for y being Surreal st y == x holds
succ A c= born y

proof

let y be Surreal; :: thesis: ( y == x implies succ A c= born y )
assume A9: ( y == x & not succ A c= born y ) ; :: thesis: contradiction
( No_uOrdinal_op (born y) < No_uOrdinal_op (succ A) & No_uOrdinal_op (succ A) == No_Ordinal_op (succ A) ) by Th75, Th73, A9, ORDINAL1:16;
then No_uOrdinal_op (born y) < No_Ordinal_op (succ A) by SURREALO:4;
then A10: No_uOrdinal_op (born y) < x by A6, SURREALO:4;
born y c= A by A9, ORDINAL1:16, ORDINAL1:22;
then ( y in Day (born y) & Day (born y) c= Day A ) by SURREAL0:35, SURREAL0:def 18;
then y <= No_uOrdinal_op (born y) by Th76;
hence contradiction by A9, A10, SURREALO:4; :: thesis: verum

end;

then A11: born_eq x = succ A by A8, SURREALO:def 5, A7, XBOOLE_0:def 10;
then A12: x in born_eq_set x by A4, SURREALO:def 6;
A13: (L_ x) \/ (R_ x) is uniq-surreal-membered ;
for z being Surreal st z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z holds
(card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z))

proof

let z be Surreal; :: thesis: ( z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z implies (card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z)) )
assume that
A14: ( z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z ) and
A15: not (card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z)) ; :: thesis: contradiction
A16: ( z == x & z in Day (succ A) ) by A11, A14, SURREALO:def 6;
then ( L_ z << {x} & L_ x << {z} ) by SURREAL0:43;
then ( ex xR being Surreal st
( xR in R_ (No_uOrdinal_op A) & No_uOrdinal_op A < xR & xR <= z ) or ex yL being Surreal st
( yL in L_ z & No_uOrdinal_op A <= yL & yL < z ) ) by SURREALO:13, SURREALO:21;
then consider zL being Surreal such that
A17: ( zL in L_ z & No_uOrdinal_op A <= zL & zL < z ) by Def10;
zL in (L_ z) \/ (R_ z) by A17, XBOOLE_0:def 3;
then A18: zL is uSurreal by A14;
zL in (L_ z) \/ (R_ z) by A17, XBOOLE_0:def 3;
then ( born zL in born z & born z c= succ A ) by SURREALO:1, A16, SURREAL0:def 18;
then ( zL in Day (born zL) & Day (born zL) c= Day A ) by SURREAL0:35, SURREAL0:def 18, ORDINAL1:22;
then zL == No_uOrdinal_op A by Th76, A17;
then A19: zL = No_uOrdinal_op A by A18, SURREALO:50;
( card (L_ x) = 1 & card (R_ x) = 0 ) by CARD_1:30;
then (card (L_ x)) (+) (card (R_ x)) = 1 by ORDINAL7:69;
then (card (L_ z)) (+) (card (R_ z)) = 1 by CARD_1:49, A15, ORDINAL1:16, A17, ZFMISC_1:33;
then consider w being Surreal such that
A20: ( z = [{},{w}] or z = [{w},{}] ) by SURREALO:47;
thus contradiction by A20, A17, A14, A19, TARSKI:def 1; :: thesis: verum

end;

then A21: x is uSurreal by A12, A13, SURREALO:49;
No_Ordinal_op (succ A) == No_uOrdinal_op (succ A) by Th73;
then No_uOrdinal_op (succ A) == x by A6, SURREALO:4;
hence No_uOrdinal_op (succ A) = [{(No_uOrdinal_op A)},{}] by A21, SURREALO:50; :: thesis: verum