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