let x, y be Surreal; :: thesis: ( x <= y iff ( L_ x << {y} & {x} << R_ y ) )
consider Ax being Ordinal such that
A1: x in Day Ax by Def14;
consider Ay being Ordinal such that
A2: y in Day Ay by Def14;
set A = Ax \/ Ay;
A3: ( Day Ax c= Day (Ax \/ Ay) & Day Ay c= Day (Ax \/ Ay) ) by XBOOLE_1:7, Th35;
then A4: ( x in Day (Ax \/ Ay) & y in Day (Ax \/ Ay) ) by A1, A2;
set S = No_Ord (Ax \/ Ay);
[:(Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay))),(Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay))):] = ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by Lm3;
then A5: ( No_Ord (Ax \/ Ay) preserves_No_Comparison_on ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) & No_Ord (Ax \/ Ay) c= ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) ) by Def12;
thus ( x <= y implies ( L_ x << {y} & {x} << R_ y ) ) :: thesis: ( L_ x << {y} & {x} << R_ y implies x <= y )

proof

assume x <= y ; :: thesis: ( L_ x << {y} & {x} << R_ y )
then x <= No_Ord (Ax \/ Ay),y by A3, A1, A2, Th40;
then A6: ( L_ x << No_Ord (Ax \/ Ay),{y} & {x} << No_Ord (Ax \/ Ay), R_ y ) by A5;
thus L_ x << {y} :: thesis: {x} << R_ y

proof

given l, r being Surreal such that A7: ( l in L_ x & r in {y} & r <= l ) ; :: according to SURREAL0:def 20 :: thesis: contradiction
A8: r = y by A7, TARSKI:def 1;
l in (L_ x) \/ (R_ x) by A7, XBOOLE_0:def 3;
then consider Ol being Ordinal such that
A9: ( Ol in Ax \/ Ay & l in Day ((No_Ord (Ax \/ Ay)),Ol) ) by A4, Th7;
Day ((No_Ord (Ax \/ Ay)),Ol) c= Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay)) by Th9, A9, ORDINAL1:def 2;
hence contradiction by A9, A6, A3, A2, A8, A7, Th40; :: thesis: verum

end;

thus {x} << R_ y :: thesis: verum

proof

given l, r being Surreal such that A10: ( l in {x} & r in R_ y & r <= l ) ; :: according to SURREAL0:def 20 :: thesis: contradiction
A11: l = x by A10, TARSKI:def 1;
r in (L_ y) \/ (R_ y) by A10, XBOOLE_0:def 3;
then consider Or being Ordinal such that
A12: ( Or in Ax \/ Ay & r in Day ((No_Ord (Ax \/ Ay)),Or) ) by A4, Th7;
Day ((No_Ord (Ax \/ Ay)),Or) c= Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay)) by Th9, A12, ORDINAL1:def 2;
hence contradiction by A3, A12, A6, A1, A11, A10, Th40; :: thesis: verum

end;

end;

assume A13: ( L_ x << {y} & {x} << R_ y ) ; :: thesis: x <= y
A14: [x,y] in ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by A3, A1, A2, Th33;
A15: L_ x << No_Ord (Ax \/ Ay),{y}

proof

given l, r being object such that A16: ( l in L_ x & r in {y} & l >= No_Ord (Ax \/ Ay),r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
[r,l] in ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by A16, A5;
then ( l in Day (Ax \/ Ay) & r in Day (Ax \/ Ay) ) by ZFMISC_1:87;
then reconsider l = l, r = r as Surreal ;
r <= l by A16;
hence contradiction by A13, A16; :: thesis: verum

end;

{x} << No_Ord (Ax \/ Ay), R_ y

proof

given l, r being object such that A17: ( l in {x} & r in R_ y & l >= No_Ord (Ax \/ Ay),r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
[r,l] in ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by A17, A5;
then ( l in Day (Ax \/ Ay) & r in Day (Ax \/ Ay) ) by ZFMISC_1:87;
then reconsider l = l, r = r as Surreal ;
r <= l by A17;
hence contradiction by A13, A17; :: thesis: verum

end;

then x <= No_Ord (Ax \/ Ay),y by A15, A14, A5;
hence x <= y ; :: thesis: verum