theorem Th62: :: FUNCT_8:62

for x being Real st x < 0 holds
absreal . x = - x