let x, y be Surreal; :: thesis: ( |.y.| infinitely< |.x.| implies not x == 0_No )
assume A1: |.y.| infinitely< |.x.| ; :: thesis: not x == 0_No
( |.x.| = x or |.x.| = - x ) by Def6;
hence not x == 0_No by SURREALR:24, A1, Th46; :: thesis: verum