let x be Surreal; :: thesis: - x <= |.x.|
( - x <= |.(- x).| & |.(- x).| == |.x.| ) by SURREALC:34, SURREALC:40;
hence - x <= |.x.| by SURREALO:9; :: thesis: verum