theorem Th53: :: JGRAPH_6:53

for a, b, c, d being Real st a < b & c < d holds
ex f being Function of I[01],((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) st
( f is being_homeomorphism & f . 0 = W-min (rectangle (a,b,c,d)) & f . 1 = E-max (rectangle (a,b,c,d)) & rng f = Upper_Arc (rectangle (a,b,c,d)) & ( for r being Real st r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( for r being Real st r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg (|[a,c]|,|[a,d]|) holds
( 0 <= (((p `2) - c) / (d - c)) / 2 & (((p `2) - c) / (d - c)) / 2 <= 1 & f . ((((p `2) - c) / (d - c)) / 2) = p ) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg (|[a,d]|,|[b,d]|) holds
( 0 <= ((((p `1) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f . (((((p `1) - a) / (b - a)) / 2) + (1 / 2)) = p ) ) )