:: deftheorem Def6 defines |. SURREALC:def 6 :
for x being Surreal holds
( ( 0_No <= x implies |.x.| = x ) & ( not 0_No <= x implies |.x.| = - x ) );