theorem :: SURREALC:32

for x being Surreal holds
( |.x.| = x or |.x.| = - x ) by Def6;