let a be R_eal; :: thesis: ( ( for r being Real holds R_EAL r < a ) implies a = +infty )
assume A1: for r being Real holds R_EAL r < a ; :: thesis: a = +infty
assume not a = +infty ; :: thesis: contradiction
then a < +infty by XXREAL_0:4;
then consider b being R_eal such that
A2: ( a < b & b < +infty & b in REAL ) by MEASURE5:17;
reconsider b = b as Real by A2;
a <= R_EAL b by A2;
hence contradiction by A1; :: thesis: verum