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;
for y being real number st y in rng f holds
a <= y

proof

let y be real number ; :: thesis: ( y in rng f implies 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 SEQ_4:def 2; :: thesis: verum