for x being ExtReal holds
( |.x.| < +infty iff x in REAL ) by Th19, Th28, XXREAL_0:4, XXREAL_0:14;