theorem Th15: :: INTEGRA5:15

for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )