theorem Th12: :: XXREAL_0:12

for a being ExtReal st a in REAL holds
-infty < a