theorem Th54: :: JGRAPH_6:54

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