let X be real-membered set ; :: thesis: ( X is right_end implies X is bounded_above )

assume sup X in X ; :: according to XXREAL_2:def 6 :: thesis: X is bounded_above

then reconsider r = sup X as Real ;

take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of X

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= r )

thus ( x in X implies x <= r ) by Th4; :: thesis: verum

assume sup X in X ; :: according to XXREAL_2:def 6 :: thesis: X is bounded_above

then reconsider r = sup X as Real ;

take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of X

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= r )

thus ( x in X implies x <= r ) by Th4; :: thesis: verum