let X be real-membered non empty set ; :: thesis: ( X is bounded_above implies sup X in REAL )
given r being real number such that G: r is UpperBound of X ; :: according to XXREAL_2:def 10 :: thesis: sup X in REAL
A: sup X <= r by Def3, G;
consider s being real number such that
W: s in X by MEMBERED:9;
F: ( r in REAL & s in REAL ) by XREAL_0:def 1;
s <= sup X by W, Th3B;
hence sup X in REAL by A, F, XXREAL_0:45; :: thesis: verum