theorem :: JORDAN5A:18
for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for P, Q being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)