let x be R_eal; :: thesis: |.x.| = |.(- x).|

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

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

then |.(- x).| = - (- x) by EXTREAL1:37
.= x ;
hence |.x.| = |.(- x).| by A1, EXTREAL1:36; :: thesis: verum

end;

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

then |.x.| = - x by EXTREAL1:37;
hence |.x.| = |.(- x).| by A2, EXTREAL1:36; :: thesis: verum

end;

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

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

end;

end;