let a be R_eal; :: thesis: ( ( for r being Real holds a < r ) implies a = -infty )
assume A1: for r being Real holds a < r ; :: thesis: a = -infty
assume A2: not a = -infty ; :: thesis: contradiction
-infty <= a by XXREAL_0:5;
then -infty < a by A2, XXREAL_0:1;
then consider b being R_eal such that
-infty < b and
A3: b < a and
A4: b in REAL by MEASURE5:2;
reconsider b = b as Real by A4;
b <= a by A3;
hence contradiction by A1; :: thesis: verum