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

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

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

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

end;

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

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

end;

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

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

end;

end;