theorem Th13: :: SURREALO:13

for x, y being Surreal holds
( 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 ) )