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 number ;
take r ; :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of X
let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= r )
thus ( x in X implies x <= r ) by Th3B; :: thesis: verum