let X be natural-membered set ; :: thesis: X is bounded_below
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies 0 <= x )
assume x in X ; :: thesis: 0 <= x
hence 0 <= x ; :: thesis: verum