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

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