theorem :: EXTREAL1:14

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