theorem ABS1: :: NEWTON05:3

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