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

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