let x be Surreal; :: thesis: ( born x = born_eq x & not born x is limit_ordinal implies ex y, z being Surreal st
( x == z & ( z = [((L_ y) \/ {y}),(R_ y)] or z = [(L_ y),((R_ y) \/ {y})] ) ) )
assume A1: ( born x = born_eq x & not born x is limit_ordinal ) ; :: thesis: ex y, z being Surreal st
( x == z & ( z = [((L_ y) \/ {y}),(R_ y)] or z = [(L_ y),((R_ y) \/ {y})] ) )
then consider B being Ordinal such that
A2: born x = succ B by ORDINAL1:29;
defpred S₁[ object ] means for z being Surreal st z = $1 holds
( born z in B & z < x );
consider L being set such that
A3: for o being object holds
( o in L iff ( o in Day B & S₁[o] ) ) from XBOOLE_0:sch 1();
defpred S₂[ object ] means for z being Surreal st z = $1 holds
( born z in B & x < z );
consider R being set such that
A4: for o being object holds
( o in R iff ( o in Day B & S₂[o] ) ) from XBOOLE_0:sch 1();
A5: L << R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in L or not b₁ in R or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in L or not r in R or not l >= r )
assume A6: ( l in L & r in R ) ; :: thesis: not l >= r
( l < x & x <= r ) by A3, A4, A6;
hence not l >= r by Th4; :: thesis: verum

end;

A7: for o being object st o in L \/ R holds
ex O being Ordinal st
( O in B & o in Day O )

proof

let o be object ; :: thesis: ( o in L \/ R implies ex O being Ordinal st
( O in B & o in Day O ) )
assume A8: o in L \/ R ; :: thesis: ex O being Ordinal st
( O in B & o in Day O )
A9: ( o in L or o in R ) by A8, XBOOLE_0:def 3;
then o in Day B by A3, A4;
then reconsider o = o as Surreal ;
( born o in B & o in Day (born o) ) by A9, A3, A4, SURREAL0:def 18;
hence ex O being Ordinal st
( O in B & o in Day O ) ; :: thesis: verum

end;

then A10: [L,R] in Day B by A5, SURREAL0:46;
then reconsider LR = [L,R] as Surreal ;
A11: not LR == x

proof

assume LR == x ; :: thesis: contradiction
then ( born x = born_eq LR & born_eq LR c= born LR & born LR c= B ) by A1, A10, SURREAL0:def 18, Th33, Def5;
then ( succ B c= B & B c= succ B ) by A2, XBOOLE_1:1, XBOOLE_1:7;
then succ B = B by XBOOLE_0:def 10;
then B in B by ORDINAL1:6;
hence contradiction ; :: thesis: verum

end;

per cases ( LR < x or x < LR ) by A11;

suppose A12: LR < x ; :: thesis: ex y, z being Surreal st
( x == z & ( z = [((L_ y) \/ {y}),(R_ y)] or z = [(L_ y),((R_ y) \/ {y})] ) )

A13: L \/ {LR} << R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in L \/ {LR} or not b₁ in R or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in L \/ {LR} or not r in R or not l >= r )
assume A14: ( l in L \/ {LR} & r in R ) ; :: thesis: not l >= r
( l in L or l = LR ) by A14, ZFMISC_1:136;
then ( l < x & x <= r ) by A12, A3, A4, A14;
hence not l >= r by Th4; :: thesis: verum

end;

for o being object st o in (L \/ {LR}) \/ R holds
ex O being Ordinal st
( O in succ B & o in Day O )

proof

let o be object ; :: thesis: ( o in (L \/ {LR}) \/ R implies ex O being Ordinal st
( O in succ B & o in Day O ) )
assume A15: o in (L \/ {LR}) \/ R ; :: thesis: ex O being Ordinal st
( O in succ B & o in Day O )
( o in L \/ {LR} or o in R ) by A15, XBOOLE_0:def 3;
then A16: ( o in L or o = LR or o in R ) by ZFMISC_1:136;
then ( o = LR or o in Day B ) by A3, A4;
then reconsider o = o as Surreal ;
( born o in B or born o c= B ) by A10, A16, A3, A4, SURREAL0:def 18;
then born o c= B by ORDINAL1:def 2;
then ( born o in succ B & o in Day (born o) ) by ORDINAL1:22, SURREAL0:def 18;
hence ex O being Ordinal st
( O in succ B & o in Day O ) ; :: thesis: verum

end;

then A17: [(L \/ {LR}),R] in Day (succ B) by A13, SURREAL0:46;
then reconsider L1R = [(L \/ {LR}),R] as Surreal ;
take LR ; :: thesis: ex z being Surreal st
( x == z & ( z = [((L_ LR) \/ {LR}),(R_ LR)] or z = [(L_ LR),((R_ LR) \/ {LR})] ) )
take L1R ; :: thesis: ( x == L1R & ( L1R = [((L_ LR) \/ {LR}),(R_ LR)] or L1R = [(L_ LR),((R_ LR) \/ {LR})] ) )
not born L1R c= B

proof

assume A18: born L1R c= B ; :: thesis: contradiction
LR in L \/ {LR} by ZFMISC_1:136;
then LR in (L_ L1R) \/ (R_ L1R) by XBOOLE_0:def 3;
then born LR in born L1R by Th1;
then S₁[LR] by A12, A18;
then ( LR in L & L = L_ LR & L_ LR << {LR} & LR in {LR} ) by A3, A7, A5, SURREAL0:46, Th11, TARSKI:def 1;
hence contradiction by Th3; :: thesis: verum

end;

then A19: ( succ B c= born L1R & born L1R c= succ B ) by A17, ORDINAL1:16, ORDINAL1:21, SURREAL0:def 18;
for y being Surreal st y == L1R holds
succ B c= born y

proof

let y be Surreal; :: thesis: ( y == L1R implies succ B c= born y )
assume A20: y == L1R ; :: thesis: succ B c= born y
assume A21: not succ B c= born y ; :: thesis: contradiction
then A22: born y c= B by ORDINAL1:16, ORDINAL1:22;
A23: ( L_ L1R << {y} & {y} << R_ L1R ) by A20, SURREAL0:43;
( LR in L \/ {LR} & y in {y} ) by TARSKI:def 1, ZFMISC_1:136;

per cases then ( ex xLR being Surreal st
( xLR in R_ LR & LR < xLR & xLR <= y ) or ex yL being Surreal st
( yL in L_ y & LR <= yL & yL < y ) ) by Th13, A23;

suppose ex xLR being Surreal st
( xLR in R_ LR & LR < xLR & xLR <= y ) ; :: thesis: contradiction

then consider xLR being Surreal such that
A24: ( xLR in R_ LR & LR < xLR & xLR <= y ) ;
xLR <= L1R by A20, A24, Th4;
then ( L_ xLR << {L1R} & {xLR} << R_ L1R ) by SURREAL0:43;
then ( xLR in {xLR} & {xLR} << R ) by TARSKI:def 1;
hence contradiction by Th3, A24; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in L_ y & LR <= yL & yL < y ) ; :: thesis: contradiction

then consider yL being Surreal such that
A25: ( yL in L_ y & LR <= yL & yL < y ) ;
yL in (L_ y) \/ (R_ y) by A25, XBOOLE_0:def 3;
then A26: born yL in born y by Th1;
then A27: ( yL in Day (born yL) & Day (born yL) c= Day B ) by A21, ORDINAL1:22, SURREAL0:def 18, SURREAL0:35;

per cases ( x == yL or yL < x or x < yL ) ;

suppose x == yL ; :: thesis: contradiction

then ( B in succ B & succ B in B ) by A2, A26, A22, A1, ORDINAL1:6, ORDINAL1:12, Def5;
hence contradiction ; :: thesis: verum

end;

suppose yL < x ; :: thesis: contradiction

then S₁[yL] by A26, A22;
then ( yL in L & L = L_ LR & L_ LR << {LR} & LR in {LR} ) by A3, A27, TARSKI:def 1, Th11;
hence contradiction by A25; :: thesis: verum

end;

suppose x < yL ; :: thesis: contradiction

then S₂[yL] by A26, A22;
then ( yL in R & L1R in {L1R} & {L1R} << R_ L1R ) by A4, A27, TARSKI:def 1, Th11;
then ( L1R <= yL & yL < L1R ) by A25, A20, Th4;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

then A28: born_eq L1R = succ B by A19, XBOOLE_0:def 10, Def5;
A29: L_ L1R << {x}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in L_ L1R or not b₁ in {x} or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in L_ L1R or not r in {x} or not l >= r )
assume A30: ( l in L_ L1R & r in {x} ) ; :: thesis: not l >= r
( l in L or l = LR ) by A30, ZFMISC_1:136;
then l < x by A12, A3;
hence not l >= r by A30, TARSKI:def 1; :: thesis: verum

end;

A31: {L1R} << R_ x

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in {L1R} or not b₁ in R_ x or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in {L1R} or not r in R_ x or not l >= r )
assume A32: ( l in {L1R} & r in R_ x ) ; :: thesis: not l >= r
A33: r in (L_ x) \/ (R_ x) by A32, XBOOLE_0:def 3;
then A34: born r c= B by Th1, A2, ORDINAL1:22;
A35: ( x in {x} & {x} << R_ x ) by Th11, TARSKI:def 1;
A36: l = L1R by A32, TARSKI:def 1;
assume A37: r <= l ; :: thesis: contradiction
not l <= r

proof

assume l <= r ; :: thesis: contradiction
then L1R == r by A37, A32, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A33, Th1, Th33, Def5;
hence contradiction by A28, ORDINAL1:12; :: thesis: verum

end;

per cases then ( ex xR being Surreal st
( xR in R_ r & r < xR & xR <= L1R ) or ex yL being Surreal st
( yL in L_ L1R & r <= yL & yL < L1R ) ) by A36, Th13;

suppose ex xR being Surreal st
( xR in R_ r & r < xR & xR <= L1R ) ; :: thesis: contradiction

then consider xR being Surreal such that
A38: ( xR in R_ r & r < xR & xR <= L1R ) ;
xR in (L_ r) \/ (R_ r) by A38, XBOOLE_0:def 3;
then A39: born xR in born r by Th1;
then A40: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A34, SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;
r <= xR by A38;
then S₂[xR] by A35, A32, Th4, A39, A34;
then ( xR in R & L1R in {L1R} & {L1R} << R_ L1R ) by TARSKI:def 1, Th11, A40, A4;
hence contradiction by A38; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in L_ L1R & r <= yL & yL < L1R ) ; :: thesis: contradiction

then consider yL being Surreal such that
A41: ( yL in L_ L1R & r <= yL & yL < L1R ) ;

per cases ( yL in L or yL = LR ) by A41, ZFMISC_1:136;

suppose yL in L ; :: thesis: contradiction

then yL <= x by A3;
hence contradiction by A35, A32, Th4, A41; :: thesis: verum

end;

suppose yL = LR ; :: thesis: contradiction

then ( LR <= x & x < LR ) by A12, A35, A32, A41, Th4;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

A42: L_ x << {L1R}

proof

let r be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not r in L_ x or not b₁ in {L1R} or not r >= b₁ )
let l be Surreal; :: thesis: ( not r in L_ x or not l in {L1R} or not r >= l )
assume A43: ( r in L_ x & l in {L1R} ) ; :: thesis: not r >= l
A44: r in (L_ x) \/ (R_ x) by A43, XBOOLE_0:def 3;
then A45: born r c= B by Th1, A2, ORDINAL1:22;
A46: ( x in {x} & L_ x << {x} ) by Th11, TARSKI:def 1;
A47: l = L1R by A43, TARSKI:def 1;
assume A48: l <= r ; :: thesis: contradiction
not r <= l

proof

assume r <= l ; :: thesis: contradiction
then L1R == r by A48, A43, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A44, Th1, Th33, Def5;
hence contradiction by A28, ORDINAL1:12; :: thesis: verum

end;

per cases then ( ex xR being Surreal st
( xR in L_ r & L1R <= xR & xR < r ) or ex yL being Surreal st
( yL in R_ L1R & L1R < yL & yL <= r ) ) by A47, Th13;

suppose ex xR being Surreal st
( xR in L_ r & L1R <= xR & xR < r ) ; :: thesis: contradiction

then consider xR being Surreal such that
A49: ( xR in L_ r & L1R <= xR & xR < r ) ;
xR in (L_ r) \/ (R_ r) by A49, XBOOLE_0:def 3;
then A50: born xR in born r by Th1;
then A51: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A45, ORDINAL1:def 2, SURREAL0:def 18, SURREAL0:35;
xR <= r by A49;
then S₁[xR] by A50, A45, A46, A43, Th4;
then xR in L by A51, A3;
then ( xR in L_ L1R & L1R in {L1R} & L_ L1R << {L1R} ) by XBOOLE_0:def 3, TARSKI:def 1, Th11;
hence contradiction by A49; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in R_ L1R & L1R < yL & yL <= r ) ; :: thesis: contradiction

then consider yL being Surreal such that
A52: ( yL in R_ L1R & L1R < yL & yL <= r ) ;
x <= yL by A4, A52;
hence contradiction by A52, A46, A43, Th4; :: thesis: verum

end;

end;

end;

{x} << R_ L1R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in {x} or not b₁ in R_ L1R or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in {x} or not r in R_ L1R or not l >= r )
assume A53: ( l in {x} & r in R_ L1R ) ; :: thesis: not l >= r
x < r by A4, A53;
hence not l >= r by A53, TARSKI:def 1; :: thesis: verum

end;

hence ( x == L1R & ( L1R = [((L_ LR) \/ {LR}),(R_ LR)] or L1R = [(L_ LR),((R_ LR) \/ {LR})] ) ) by A31, SURREAL0:43, A29, A42; :: thesis: verum

end;

suppose A54: x < LR ; :: thesis: ex y, z being Surreal st
( x == z & ( z = [((L_ y) \/ {y}),(R_ y)] or z = [(L_ y),((R_ y) \/ {y})] ) )

A55: L << R \/ {LR}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in L or not b₁ in R \/ {LR} or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in L or not r in R \/ {LR} or not l >= r )
assume A56: ( l in L & r in R \/ {LR} ) ; :: thesis: not l >= r
( r in R or r = LR ) by A56, ZFMISC_1:136;
then ( l <= x & x < r ) by A54, A3, A4, A56;
hence not l >= r by Th4; :: thesis: verum

end;

for o being object st o in L \/ (R \/ {LR}) holds
ex O being Ordinal st
( O in succ B & o in Day O )

proof

let o be object ; :: thesis: ( o in L \/ (R \/ {LR}) implies ex O being Ordinal st
( O in succ B & o in Day O ) )
assume A57: o in L \/ (R \/ {LR}) ; :: thesis: ex O being Ordinal st
( O in succ B & o in Day O )
( o in L or o in R \/ {LR} ) by A57, XBOOLE_0:def 3;
then A58: ( o in L or o = LR or o in R ) by ZFMISC_1:136;
then ( o = LR or o in Day B ) by A3, A4;
then reconsider o = o as Surreal ;
( born o in B or born o c= B ) by A10, A58, A3, A4, SURREAL0:def 18;
then born o c= B by ORDINAL1:def 2;
then ( born o in succ B & o in Day (born o) ) by ORDINAL1:22, SURREAL0:def 18;
hence ex O being Ordinal st
( O in succ B & o in Day O ) ; :: thesis: verum

end;

then A59: [L,(R \/ {LR})] in Day (succ B) by A55, SURREAL0:46;
then reconsider L1R = [L,(R \/ {LR})] as Surreal ;
take LR ; :: thesis: ex z being Surreal st
( x == z & ( z = [((L_ LR) \/ {LR}),(R_ LR)] or z = [(L_ LR),((R_ LR) \/ {LR})] ) )
take L1R ; :: thesis: ( x == L1R & ( L1R = [((L_ LR) \/ {LR}),(R_ LR)] or L1R = [(L_ LR),((R_ LR) \/ {LR})] ) )
not born L1R c= B

proof

assume A60: born L1R c= B ; :: thesis: contradiction
LR in R \/ {LR} by ZFMISC_1:136;
then LR in (L_ L1R) \/ (R_ L1R) by XBOOLE_0:def 3;
then born LR in born L1R by Th1;
then S₂[LR] by A54, A60;
then ( LR in R & R = R_ LR & {LR} << R_ LR & LR in {LR} ) by A4, A7, A5, SURREAL0:46, Th11, TARSKI:def 1;
hence contradiction by Th3; :: thesis: verum

end;

then A61: ( succ B c= born L1R & born L1R c= succ B ) by A59, ORDINAL1:16, ORDINAL1:21, SURREAL0:def 18;
for y being Surreal st y == L1R holds
succ B c= born y

proof

let y be Surreal; :: thesis: ( y == L1R implies succ B c= born y )
assume A62: y == L1R ; :: thesis: succ B c= born y
assume A63: not succ B c= born y ; :: thesis: contradiction
then A64: born y c= B by ORDINAL1:16, ORDINAL1:22;
A65: ( L_ L1R << {y} & {y} << R_ L1R ) by A62, SURREAL0:43;
( LR in R \/ {LR} & y in {y} ) by TARSKI:def 1, ZFMISC_1:136;

per cases then ( ex xLR being Surreal st
( xLR in L_ LR & y <= xLR & xLR < LR ) or ex yL being Surreal st
( yL in R_ y & y < yL & yL <= LR ) ) by A65, Th13;

suppose ex xLR being Surreal st
( xLR in L_ LR & y <= xLR & xLR < LR ) ; :: thesis: contradiction

then consider xLR being Surreal such that
A66: ( xLR in L_ LR & y <= xLR & xLR < LR ) ;
L1R <= xLR by A62, A66, Th4;
then ( L_ L1R << {xLR} & {L1R} << R_ xLR ) by SURREAL0:43;
then ( L << {xLR} & xLR in {xLR} ) by TARSKI:def 1;
hence contradiction by Th3, A66; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in R_ y & y < yL & yL <= LR ) ; :: thesis: contradiction

then consider yL being Surreal such that
A67: ( yL in R_ y & y < yL & yL <= LR ) ;
yL in (L_ y) \/ (R_ y) by A67, XBOOLE_0:def 3;
then A68: born yL in born y by Th1;
then A69: ( yL in Day (born yL) & Day (born yL) c= Day B ) by A63, ORDINAL1:22, SURREAL0:def 18, SURREAL0:35;

per cases ( x == yL or x < yL or yL < x ) ;

suppose x == yL ; :: thesis: contradiction

then ( B in succ B & succ B in B ) by A2, A68, A64, A1, Def5, ORDINAL1:6, ORDINAL1:12;
hence contradiction ; :: thesis: verum

end;

suppose x < yL ; :: thesis: contradiction

then S₂[yL] by A68, A64;
then ( yL in R & R = R_ LR & {LR} << R_ LR & LR in {LR} ) by A4, A69, TARSKI:def 1, Th11;
hence contradiction by A67; :: thesis: verum

end;

suppose yL < x ; :: thesis: contradiction

then S₁[yL] by A68, A64;
then ( yL in L & L1R in {L1R} & L_ L1R << {L1R} ) by A3, A69, TARSKI:def 1, Th11;
then ( L1R <= yL & yL < L1R ) by A67, A62, Th4;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

then A70: born_eq L1R = succ B by A61, XBOOLE_0:def 10, Def5;
A71: L_ L1R << {x}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in L_ L1R or not b₁ in {x} or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in L_ L1R or not r in {x} or not l >= r )
assume A72: ( l in L_ L1R & r in {x} ) ; :: thesis: not l >= r
l < x by A3, A72;
hence not l >= r by A72, TARSKI:def 1; :: thesis: verum

end;

A73: {L1R} << R_ x

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in {L1R} or not b₁ in R_ x or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in {L1R} or not r in R_ x or not l >= r )
assume A74: ( l in {L1R} & r in R_ x ) ; :: thesis: not l >= r
A75: r in (L_ x) \/ (R_ x) by A74, XBOOLE_0:def 3;
then A76: born r c= B by A2, Th1, ORDINAL1:22;
A77: ( x in {x} & {x} << R_ x ) by Th11, TARSKI:def 1;
A78: l = L1R by A74, TARSKI:def 1;
assume A79: r <= l ; :: thesis: contradiction
not l <= r

proof

assume l <= r ; :: thesis: contradiction
then L1R == r by A79, A74, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A75, Th1, Th33, Def5;
hence contradiction by A70, ORDINAL1:12; :: thesis: verum

end;

per cases then ( ex xR being Surreal st
( xR in R_ r & r < xR & xR <= L1R ) or ex yL being Surreal st
( yL in L_ L1R & r <= yL & yL < L1R ) ) by A78, Th13;

suppose ex xR being Surreal st
( xR in R_ r & r < xR & xR <= L1R ) ; :: thesis: contradiction

then consider xR being Surreal such that
A80: ( xR in R_ r & r < xR & xR <= L1R ) ;
xR in (L_ r) \/ (R_ r) by A80, XBOOLE_0:def 3;
then A81: born xR in born r by Th1;
then A82: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A76, SURREAL0:def 18, SURREAL0:35, ORDINAL1:def 2;
r <= xR by A80;
then S₂[xR] by A81, A76, A77, A74, Th4;
then xR in R by A82, A4;
then ( xR in R \/ {LR} & L1R in {L1R} & {L1R} << R_ L1R ) by TARSKI:def 1, Th11, XBOOLE_0:def 3;
hence contradiction by A80; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in L_ L1R & r <= yL & yL < L1R ) ; :: thesis: contradiction

then consider yL being Surreal such that
A83: ( yL in L_ L1R & r <= yL & yL < L1R ) ;
yL <= x by A3, A83;
hence contradiction by A83, A77, A74, Th4; :: thesis: verum

end;

end;

end;

A84: L_ x << {L1R}

proof

let r be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not r in L_ x or not b₁ in {L1R} or not r >= b₁ )
let l be Surreal; :: thesis: ( not r in L_ x or not l in {L1R} or not r >= l )
assume A85: ( r in L_ x & l in {L1R} ) ; :: thesis: not r >= l
A86: r in (L_ x) \/ (R_ x) by A85, XBOOLE_0:def 3;
then A87: born r c= B by A2, Th1, ORDINAL1:22;
A88: ( x in {x} & L_ x << {x} ) by Th11, TARSKI:def 1;
A89: l = L1R by A85, TARSKI:def 1;
assume A90: l <= r ; :: thesis: contradiction
not r <= l

proof

assume r <= l ; :: thesis: contradiction
then L1R == r by A90, A85, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A86, Th1, Th33, Def5;
hence contradiction by A70, ORDINAL1:12; :: thesis: verum

end;

per cases then ( ex xR being Surreal st
( xR in L_ r & L1R <= xR & xR < r ) or ex yL being Surreal st
( yL in R_ L1R & L1R < yL & yL <= r ) ) by A89, Th13;

suppose ex xR being Surreal st
( xR in L_ r & L1R <= xR & xR < r ) ; :: thesis: contradiction

then consider xR being Surreal such that
A91: ( xR in L_ r & L1R <= xR & xR < r ) ;
xR in (L_ r) \/ (R_ r) by A91, XBOOLE_0:def 3;
then A92: born xR in born r by Th1;
then A93: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A87, ORDINAL1:def 2, SURREAL0:def 18, SURREAL0:35;
xR <= r by A91;
then S₁[xR] by A92, A87, A88, A85, Th4;
then ( xR in L_ L1R & L1R in {L1R} & L_ L1R << {L1R} ) by A93, A3, TARSKI:def 1, Th11;
hence contradiction by A91; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in R_ L1R & L1R < yL & yL <= r ) ; :: thesis: contradiction

then consider yL being Surreal such that
A94: ( yL in R_ L1R & L1R < yL & yL <= r ) ;

per cases ( yL in R or yL = LR ) by A94, ZFMISC_1:136;

suppose yL in R ; :: thesis: contradiction

then x <= yL by A4;
hence contradiction by A94, A88, A85, Th4; :: thesis: verum

end;

suppose yL = LR ; :: thesis: contradiction

then ( LR <= x & x < LR ) by A54, A88, A85, A94, Th4;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

{x} << R_ L1R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in {x} or not b₁ in R_ L1R or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in {x} or not r in R_ L1R or not l >= r )
assume A95: ( l in {x} & r in R_ L1R ) ; :: thesis: not l >= r
( r in R or r = LR ) by A95, ZFMISC_1:136;
then x < r by A54, A4;
hence not l >= r by A95, TARSKI:def 1; :: thesis: verum

end;

hence ( x == L1R & ( L1R = [((L_ LR) \/ {LR}),(R_ LR)] or L1R = [(L_ LR),((R_ LR) \/ {LR})] ) ) by A73, SURREAL0:43, A71, A84; :: thesis: verum

end;

end;