let X be ext-real-membered non empty bounded_above 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 UpperBound of X by Def10;
A4: r in REAL by XREAL_0:def 1;
x <= r by A3, A1, Def1;
then x in REAL by A4, A2, XXREAL_0:13;
hence ex x being Element of REAL st x in X by A1; :: thesis: verum