let a, b be Real; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

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

suppose A1: a >= 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

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

suppose b >= 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

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

end;

suppose b < 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

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

end;

end;

end;

suppose A1: a < 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

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

suppose b >= 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

then ( |.a.| = - a & |.b.| = b ) by A1, ABSVALUE:def 1;
then |.(|.a.| - |.b.|).| = |.(- (a + b)).| ;
hence ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| ) by COMPLEX1:52; :: thesis: verum

end;

suppose b < 0 ; :: thesis: ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| )

then ( |.a.| = - a & |.b.| = - b ) by A1, ABSVALUE:def 1;
then |.(|.a.| - |.b.|).| = |.(- (a - b)).| ;
hence ( |.(|.a.| - |.b.|).| = |.(a + b).| or |.(|.a.| - |.b.|).| = |.(a - b).| ) by COMPLEX1:52; :: thesis: verum

end;

end;

end;

end;