let x, y be Surreal; :: thesis: ( x < y iff x - y < 0_No )
y = 0_No + y ;
hence ( x < y iff x - y < 0_No ) by Th41; :: thesis: verum