let x, y be Surreal; :: thesis: ( not x == 0_No & y == 0_No implies y infinitely< |.x.| )
assume A1: ( not x == 0_No & y == 0_No ) ; :: thesis: y infinitely< |.x.|
then A2: |.x.| is positive by Th36;
let r be positive Real; :: according to SURREALC:def 3 :: thesis: y * (uReal . r) < |.x.|
( (uReal . r) * y == (uReal . r) * 0_No & (uReal . r) * 0_No = 0_No ) by A1, SURREALR:51;
hence y * (uReal . r) < |.x.| by SURREALO:4, A2; :: thesis: verum