let X be real-membered non empty set ; :: thesis: ( X is bounded_above implies sup X in REAL )
given r being Real such that A1: r is UpperBound of X ; :: according to XXREAL_2:def 10 :: thesis: sup X in REAL
consider s being Real such that
A2: s in X by MEMBERED:9;
A3: s <= sup X by A2, Th4;
A4: r in REAL by XREAL_0:def 1;
A5: s in REAL by XREAL_0:def 1;
sup X <= r by A1, Def3;
hence sup X in REAL by A4, A5, A3, XXREAL_0:45; :: thesis: verum