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

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

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

then a * b >= 0 ;
hence ( |.(a + b).| = |.a.| + |.b.| or |.(a - b).| = |.a.| + |.b.| ) by ABSVALUE:11; :: thesis: verum

end;

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

then a * (- b) >= 0 ;
then |.(a + (- b)).| = |.a.| + |.(- b).| by ABSVALUE:11;
hence ( |.(a + b).| = |.a.| + |.b.| or |.(a - b).| = |.a.| + |.b.| ) by COMPLEX1:52; :: thesis: verum

end;

end;