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

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