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

proof

let x1 be set ; :: thesis: ( x1 in X /\ (dom f) implies a <= f . x1 )
A2: X /\ (dom f) = dom f by XBOOLE_1:28;
assume x1 in X /\ (dom f) ; :: thesis: a <= f . x1
then f . x1 in rng f by A2, FUNCT_1:def 5;
hence a <= f . x1 by A1; :: thesis: verum

end;

hence f | X is bounded_below by RFUNCT_1:88; :: thesis: verum