let x be Surreal; :: thesis:
assume A1: 0_No < x ; :: thesis:
defpred S₁[ object ] means for z being Surreal st z = $1 holds
0_No < z;
consider yL being set such that
A2: for o being object holds
( o in yL iff ( o in L_ x & S₁[o] ) ) from XBOOLE_0:sch 1();
consider yR being set such that
A3: for o being object holds
( o in yR iff ( o in R_ x & S₁[o] ) ) from XBOOLE_0:sch 1();
set YL = yL \/ {0_No};
A4: yL \/ {0_No} << yR

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A5: ( l in yL \/ {0_No} & r in yR ) ; :: thesis:

per cases by A5, ZFMISC_1:136;

suppose A6: l in yL ; :: thesis:

A7: L_ x << R_ x by SURREAL0:45;
( l in L_ x & r in R_ x ) by A6, A5, A2, A3;
hence not r <= l by A7; :: thesis:

end;

suppose l = 0_No ; :: thesis:

hence not r <= l by A3, A5; :: thesis:

end;

end;

end;

A8: for o being object st o in (yL \/ {0_No}) \/ yR holds
ex O being Ordinal st
( O in born x & o in Day O )

let o be object ; :: thesis:
assume o in (yL \/ {0_No}) \/ yR ; :: thesis:
then ( o in yL \/ {0_No} or o in yR ) by XBOOLE_0:def 3;
then A9: ( o in yL or o = 0_No or o in yR ) by ZFMISC_1:136;
then reconsider o = o as Surreal by SURREAL0:def 16, A2, A3;
take born o ; :: thesis:
0_No <= 0_No ;
then born x <> {} by A1, SURREAL0:37;
then {} c< born x by XBOOLE_1:2, XBOOLE_0:def 8;
then A10: {} in born x by ORDINAL1:11;
( o in L_ x or o = 0_No or o in R_ x ) by A9, A2, A3;
then ( o in (L_ x) \/ (R_ x) or o = 0_No ) by XBOOLE_0:def 3;
hence ( born o in born x & o in Day (born o) ) by SURREAL0:def 18, A10, SURREAL0:37, SURREALO:1; :: thesis:

end;

[(yL \/ {0_No}),yR] in Day (born x) by A4, A8, SURREAL0:46;
then reconsider y = [(yL \/ {0_No}),yR] as Surreal ;
take y ; :: thesis:
A11: x = [(L_ x),(R_ x)] ;
A12: for a being Surreal st a in yL \/ {0_No} holds
ex b being Surreal st
( b in L_ x & a <= b )

let a be Surreal; :: thesis:
( ex xR being Surreal st
( xR in R_ 0_No & 0_No < xR & xR <= x ) or ex yL being Surreal st
( yL in L_ x & 0_No <= yL & yL < x ) ) by A1, SURREALO:13;
then consider L being Surreal such that
A13: ( L in L_ x & 0_No <= L & L < x ) ;
assume a in yL \/ {0_No} ; :: thesis:
then ( a in yL or a = 0_No ) by ZFMISC_1:136;
hence ex b being Surreal st
( b in L_ x & a <= b ) by A13, A2; :: thesis:

end;

A14: for a being Surreal st a in R_ x holds
ex b being Surreal st
( b in yR & b <= a )

let a be Surreal; :: thesis:
assume A15: a in R_ x ; :: thesis:
0_No <= x by A1;
then ( 0_No in {0_No} & {0_No} << R_ x ) by SURREAL0:43, TARSKI:def 1;
then S₁[a] by A15;
hence ex b being Surreal st
( b in yR & b <= a ) by A15, A3; :: thesis:

end;

A16: for a being Surreal st a in yR holds
ex b being Surreal st
( b in R_ x & b <= a ) by A3;
for a being Surreal st a in L_ x holds
ex b being Surreal st
( b in yL \/ {0_No} & a <= b )

let a be Surreal; :: thesis:
assume A17: a in L_ x ; :: thesis:

suppose 0_No < a ; :: thesis:

then S₁[a] ;
then a in yL \/ {0_No} by A2, A17, ZFMISC_1:136;
hence ex b being Surreal st
( b in yL \/ {0_No} & a <= b ) ; :: thesis:

end;

suppose A18: a <= 0_No ; :: thesis:

0_No in yL \/ {0_No} by ZFMISC_1:136;
hence ex b being Surreal st
( b in yL \/ {0_No} & a <= b ) by A18; :: thesis:

end;

end;

end;

hence y == x by A14, A12, SURREAL0:44, A16, A11; :: thesis:
thus for z being Surreal holds
( z in L_ y iff ( z = 0_No or ( z in L_ x & 0_No < z ) ) ) :: thesis:

let z be Surreal; :: thesis:
thus ( not z in L_ y or z = 0_No or ( z in L_ x & 0_No < z ) ) :: thesis:

assume ( z in L_ y & z <> 0_No ) ; :: thesis:
then z in yL by ZFMISC_1:136;
hence ( z in L_ x & 0_No < z ) by A2; :: thesis:

end;

assume A19: ( z = 0_No or ( z in L_ x & 0_No < z ) ) ; :: thesis:
assume A20: not z in L_ y ; :: thesis:
then S₁[z] by A19, ZFMISC_1:136;
hence contradiction by A20, A19, A2, ZFMISC_1:136; :: thesis:

end;

let z be Surreal; :: thesis:
thus ( z in R_ y implies ( z in R_ x & 0_No < z ) ) by A3; :: thesis:
assume A21: ( z in R_ x & 0_No < z ) ; :: thesis:
then S₁[z] ;
hence z in R_ y by A3, A21; :: thesis: