theorem ABS: :: NEWTON05:2

for a, b being Real holds
( |.(a + b).| = |.a.| + |.b.| or |.(a - b).| = |.a.| + |.b.| )