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