let X be ext-real-membered non empty set ; :: thesis: ( X is bounded_above & X <> {-infty} implies sup X in REAL )
assume A1: X is bounded_above ; :: thesis: ( not X <> {-infty} or sup X in REAL )
then consider r being Real such that
A2: r is UpperBound of X ;
assume X <> {-infty} ; :: thesis: sup X in REAL
then A3: ex x being Element of REAL st x in X by A1, Th49;
sup X is UpperBound of X by Def3;
then A4: not sup X = -infty by A3, Def1, XXREAL_0:12;
A5: r in REAL by XREAL_0:def 1;
sup X <= r by A2, Def3;
hence sup X in REAL by A5, A4, XXREAL_0:13; :: thesis: verum