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