theorem Th18: :: INTEGRA4:18
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_above holds
rng (f | X) is bounded_above