theorem :: JORDAN5A:17

for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for P 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 & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)