theorem LmABS: :: NEWTON05:4

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