theorem Th13: :: MESFUNC1:13

for a being R_eal st ( for r being Real holds a < r ) holds
a = -infty