let x, y, z be Surreal; :: thesis: ( x <= y iff x + z <= y + z )
set Bx = born x;
set By = born y;
set Bz = born z;
set Bxz = (born x) (+) (born z);
set Byz = (born y) (+) (born z);
( (born x) (+) (born z) c= ((born x) (+) (born z)) \/ ((born y) (+) (born z)) & (born y) (+) (born z) c= ((born x) (+) (born z)) \/ ((born y) (+) (born z)) ) by XBOOLE_1:7;
hence ( x <= y iff x + z <= y + z ) by Lm5; :: thesis: verum