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