let x, y be Surreal; :: thesis: ( |.y.| infinitely< x implies not x == 0_No )
assume |.y.| infinitely< x ; :: thesis: not x == 0_No
then ( 0_No <= |.y.| & |.y.| < x ) by Th9, Th31;
hence not x == 0_No by SURREALO:4; :: thesis: verum