theorem Th2: :: XXREAL_3:2

for x being negative non real ExtReal holds x = -infty