let x, y be Surreal; :: thesis: ( x <= y iff - y <= - x )
set Bx = born x;
set By = born y;
set B = (born x) \/ (born y);
A1: ( Day (born x) c= Day ((born x) \/ (born y)) & Day (born y) c= Day ((born x) \/ (born y)) ) by SURREAL0:35, XBOOLE_1:7;
( x in Day (born x) & y in Day (born y) ) by SURREAL0:def 18;
hence ( x <= y iff - y <= - x ) by A1, Lm1; :: thesis: verum