theorem :: SURREALR:45

for x, y being Surreal holds
( x < y iff 0_No < y - x )