theorem Th1: :: EXTREAL1:12

for x being ExtReal
for a being Real st x = a holds
|.x.| = |.a.|