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