let X be ext-real-membered non empty bounded_below set ; :: thesis: ( X <> {+infty} implies ex x being Element of REAL st x in X )
assume X <> {+infty} ; :: thesis: ex x being Element of REAL st x in X
then consider x being object such that
A1: x in X and
A2: x <> +infty by ZFMISC_1:35;
reconsider x = x as ExtReal by A1;
consider r being Real such that
A3: r is LowerBound of X by Def9;
A4: r in REAL by XREAL_0:def 1;
r <= x by A3, A1, Def2;
then x in REAL by A4, A2, XXREAL_0:10;
hence ex x being Element of REAL st x in X by A1; :: thesis: verum