for x being ExtReal holds |.x.| = |.(- x).|