theorem :: SURREALC:58

for x being Surreal st |.x.| is positive holds
not x == 0_No by Def6;