theorem Th9:
for
a,
b,
d,
e,
s1,
s2,
t1,
t2 being
Real for
h being
Function of
(Closed-Interval-TSpace (a,b)),
(Closed-Interval-TSpace (d,e)) st
h is
being_homeomorphism &
h . s1 = t1 &
h . s2 = t2 &
h . b = d &
e >= d &
t1 >= t2 &
s1 in [.a,b.] &
s2 in [.a,b.] holds
s1 <= s2