let x, y be Surreal; :: thesis: ( not x < y or ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) )
assume x < y ; :: thesis: ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) )

per cases then ( not L_ y << {x} or not {y} << R_ x ) by SURREAL0:43;

suppose not L_ y << {x} ; :: thesis: ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) )

then consider l, r being Surreal such that
A1: ( l in L_ y & r in {x} & l >= r ) ;
( L_ y << {y} & y in {y} ) by Th11, TARSKI:def 1;
then ( x <= l & l < y ) by A1, TARSKI:def 1;
hence ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) ) by A1; :: thesis: verum

end;

suppose not {y} << R_ x ; :: thesis: ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) )

then consider l, r being Surreal such that
A2: ( l in {y} & r in R_ x & l >= r ) ;
( {x} << R_ x & x in {x} ) by Th11, TARSKI:def 1;
then ( x < r & r <= y ) by A2, TARSKI:def 1;
hence ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) ) by A2; :: thesis: verum

end;

end;