let x be ExtReal; :: thesis: |.x.| = |.(- x).|
reconsider x = x as R_eal by XXREAL_0:def 1;

per cases ( 0 < x or x < 0 or x = 0 ) ;

suppose 0 < x ; :: thesis: |.x.| = |.(- x).|

then |.(- x).| = - (- x) by Def1
.= x ;
hence |.x.| = |.(- x).| ; :: thesis: verum

end;

suppose x < 0 ; :: thesis: |.x.| = |.(- x).|

then |.x.| = - x by Def1;
hence |.x.| = |.(- x).| ; :: thesis: verum

end;

suppose x = 0 ; :: thesis: |.x.| = |.(- x).|

hence |.x.| = |.(- x).| ; :: thesis: verum

end;

end;