let a, b be Real; :: thesis: ( a = - b implies |.a.| = |.b.| )
assume A1: a = - b ; :: thesis: |.a.| = |.b.|

per cases ( a < 0 or a = 0 or a > 0 ) ;

suppose A2: a < 0 ; :: thesis: |.a.| = |.b.|

then b > 0 by A1;
then ( |.a.| = - a & |.b.| = b ) by A2, ABSVALUE:def 1;
hence |.a.| = |.b.| by A1; :: thesis: verum

end;

suppose a = 0 ; :: thesis: |.a.| = |.b.|

hence |.a.| = |.b.| by A1; :: thesis: verum

end;

suppose A3: a > 0 ; :: thesis: |.a.| = |.b.|

then b < 0 by A1;
then ( |.a.| = a & |.b.| = - b ) by A3, ABSVALUE:def 1;
hence |.a.| = |.b.| by A1; :: thesis: verum

end;

end;