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

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