let A be non empty closed_interval Subset of REAL; :: thesis: for X being set
for f being PartFunc of A,REAL st f | A is bounded_below holds
rng (f | X) is bounded_below
let X be set ; :: thesis: for f being PartFunc of A,REAL st f | A is bounded_below holds
rng (f | X) is bounded_below
let f be PartFunc of A,REAL; :: thesis: ( f | A is bounded_below implies rng (f | X) is bounded_below )
assume f | A is bounded_below ; :: thesis: rng (f | X) is bounded_below
then rng f is bounded_below by INTEGRA1:11;
hence rng (f | X) is bounded_below by RELAT_1:70, XXREAL_2:44; :: thesis: verum