theorem Th1: :: XXREAL_3:1

for x being positive non real ExtReal holds x = +infty