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

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