theorem Th7: :: EXTREAL1:18

for x being ExtReal st x <= 0 holds
|.x.| = - x