let x, y be Surreal; :: thesis: ( not y <= x implies x <= y )
assume A1: ( not y <= x & not x <= y ) ; :: thesis: contradiction

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

suppose not L_ x << {y} ; :: thesis: contradiction

then consider xl, Y being Surreal such that
A2: ( xl in L_ x & Y in {y} & Y <= xl ) ;
( L_ x <<= {x} & x in {x} ) by Th5, TARSKI:def 1;
then A3: xl <= x by A2;
y <= xl by A2, TARSKI:def 1;
hence contradiction by A1, A3, Th4; :: thesis: verum

end;

suppose not {x} << R_ y ; :: thesis: contradiction

then consider X, yr being Surreal such that
A4: ( X in {x} & yr in R_ y & yr <= X ) ;
( {y} <<= R_ y & y in {y} ) by Th5, TARSKI:def 1;
then A5: y <= yr by A4;
yr <= x by A4, TARSKI:def 1;
hence contradiction by A1, A5, Th4; :: thesis: verum

end;

end;