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