theorem Th13: :: XXREAL_0:13

for a, b being ExtReal st a in REAL & b <= a & not b in REAL holds
b = -infty