theorem Th18: :: EXTREAL1:29

for x being ExtReal holds |.x.| = |.(- x).|