for x being ExtReal holds
( not |.x.| = +infty or x = +infty or x = -infty )