let x, y be Surreal; :: thesis: for X1, X2, Y1, Y2 being set st ( for x being Surreal st x in X1 holds
ex y being Surreal st
( y in X2 & x <= y ) ) & ( for x being Surreal st x in Y2 holds
ex y being Surreal st
( y in Y1 & y <= x ) ) & x = [X1,Y1] & y = [X2,Y2] holds
x <= y
let X1, X2, Y1, Y2 be set ; :: thesis: ( ( for x being Surreal st x in X1 holds
ex y being Surreal st
( y in X2 & x <= y ) ) & ( for x being Surreal st x in Y2 holds
ex y being Surreal st
( y in Y1 & y <= x ) ) & x = [X1,Y1] & y = [X2,Y2] implies x <= y )
assume A1: ( ( for x being Surreal st x in X1 holds
ex y being Surreal st
( y in X2 & x <= y ) ) & ( for x being Surreal st x in Y2 holds
ex y being Surreal st
( y in Y1 & y <= x ) ) & x = [X1,Y1] & y = [X2,Y2] ) ; :: thesis: x <= y
A2: L_ x << {y}

proof

assume not L_ x << {y} ; :: thesis: contradiction
then consider l, r being Surreal such that
A3: ( l in L_ x & r in {y} & r <= l ) ;
consider z being Surreal such that
A4: ( z in L_ y & l <= z ) by A3, A1;
r = y by A3, TARSKI:def 1;
then ( L_ y << {l} & l in {l} ) by TARSKI:def 1, A3, Th43;
hence contradiction by A4; :: thesis: verum

end;

{x} << R_ y

proof

assume not {x} << R_ y ; :: thesis: contradiction
then consider l, r being Surreal such that
A5: ( l in {x} & r in R_ y & r <= l ) ;
consider z being Surreal such that
A6: z in R_ x and
A7: z <= r by A5, A1;
l = x by TARSKI:def 1, A5;
then ( r in {r} & {r} << R_ x ) by TARSKI:def 1, A5, Th43;
hence contradiction by A6, A7; :: thesis: verum

end;

hence x <= y by A2, Th43; :: thesis: verum