theorem LABS: :: NEWTON05:5

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