let x, y be Surreal; :: thesis: ( x infinitely< y implies x < y )
assume x infinitely< y ; :: thesis: x < y
then x * 1_No < y by SURREALN:48;
hence x < y ; :: thesis: verum