theorem LM86: :: DUALSP05:2

for x being Real holds |.x.| = (sgn x) * x