theorem Th61: :: FUNCT_8:61

for x being Real st x >= 0 holds
absreal . x = x