let A be ext-real-membered set ; :: thesis: ( A is right_end implies not A is empty )
assume sup A in A ; :: according to XXREAL_2:def 6 :: thesis: not A is empty
hence not A is empty ; :: thesis: verum