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