let X be ext-natural-membered set ; :: thesis: X is bounded_below
for x being ExtReal st x in X holds
0 <= x ;
then 0 is LowerBound of X by XXREAL_2:def 2;
hence X is bounded_below by XXREAL_2:def 9; :: thesis: verum