let a be R_eal; :: thesis: ( ( for r being Real holds r < a ) implies a = +infty )
assume A1: for r being Real holds 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 and
b < +infty and
A3: b in REAL by MEASURE5:2;
reconsider b = b as Real by A3;
a <= b by A2;
hence contradiction by A1; :: thesis: verum