theorem :: ABSVALUE:12

for x, y being Real st |.(x + y).| = |.x.| + |.y.| holds
0 <= x * y