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 number such that
A2: r is UpperBound of X by Def10;
A3: sup X <= r by A2, Def3;
X: r in REAL by XREAL_0:def 1;
assume X <> {-infty } ; :: thesis: sup X in REAL
then consider x being Element of REAL such that
A4: x in X by A1, Th49;
sup X is UpperBound of X by Def3;
then not sup X = -infty by A4, Def1, XXREAL_0:12;
hence sup X in REAL by A3, X, XXREAL_0:13; :: thesis: verum