theorem Th19: :: INTEGRA4:19

for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of A,REAL st f | A is bounded_below holds
rng (f | X) is bounded_below