for f, g being Function of I[01],(TOP-REAL 2)
for a, b, c, d being Real
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds
( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds
( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) holds
rng f meets rng g