let x, z be Surreal; :: thesis: ( |.x.| infinitely< z implies |.(- x).| infinitely< z )
assume A1: |.x.| infinitely< z ; :: thesis: |.(- x).| infinitely< z
let r be positive Real; :: according to SURREALC:def 3 :: thesis: |.(- x).| * (uReal . r) < z
( |.(- x).| * (uReal . r) == |.x.| * (uReal . r) & |.x.| * (uReal . r) < z ) by Th40, A1, SURREALR:51;
hence |.(- x).| * (uReal . r) < z by SURREALO:4; :: thesis: verum