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 A2: not a = +infty ; :: thesis: contradiction
A3: a < +infty by A2, XXREAL_0:4;
consider b being R_eal such that
A4: a < b and
b < +infty and
A5: b in REAL by A3, MEASURE5:17;
reconsider b = b as Real by A5;
A6: a <= R_EAL b by A4;
thus contradiction by A1, A6; :: thesis: verum