theorem :: XXREAL_0:14

for a being ExtReal holds
( a in REAL or a = +infty or a = -infty ) by Lm10;