theorem Th9: :: XXREAL_0:9

for a being ExtReal st a in REAL holds
+infty > a