theorem Th12: :: MESFUNC1:12

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