let X be non empty set ; :: thesis: for f being PartFunc of X,REAL st f | X is bounded_below holds
rng f is bounded_below
let f be PartFunc of X,REAL; :: thesis: ( f | X is bounded_below implies rng f is bounded_below )
assume f | X is bounded_below ; :: thesis: rng f is bounded_below
then consider a being real number such that
A1: for x1 being set st x1 in X /\ (dom f) holds
a <= f . x1 by RFUNCT_1:88;
A2: X /\ (dom f) = dom f by XBOOLE_1:28;
a is LowerBound of rng f

proof

let y be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not y in rng f or a <= y )
assume y in rng f ; :: thesis: a <= y
then ex s being set st
( s in dom f & y = f . s ) by FUNCT_1:def 5;
hence a <= y by A1, A2; :: thesis: verum

end;

hence rng f is bounded_below by XXREAL_2:def 9; :: thesis: verum