let X be real-membered set ; :: thesis: ( X is left_end implies X is bounded_below )
assume inf X in X ; :: according to XXREAL_2:def 5 :: thesis: X is bounded_below
then reconsider r = inf X as Real ;
take r ; :: according to XXREAL_2:def 9 :: thesis: r is LowerBound of X
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies r <= x )
thus ( x in X implies r <= x ) by Th3; :: thesis: verum