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