let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: for a, b, c, d being real number
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 & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds
( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) holds
rng f meets rng g
let a, b, c, d be real number ; :: thesis: 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 & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds
( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) holds
rng f meets rng g
let O, I be Point of I[01] ; :: thesis: ( 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 & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds
( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) implies rng f meets rng g )
assume A1: ( 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 & (g . O) `2 = c & (g . I) `2 = d & ( for r being Point of I[01] holds
( a <= (f . r) `1 & (f . r) `1 <= b & a <= (g . r) `1 & (g . r) `1 <= b & c <= (f . r) `2 & (f . r) `2 <= d & c <= (g . r) `2 & (g . r) `2 <= d ) ) ) ; :: thesis: rng f meets rng g
reconsider P = rng f as non empty Subset of (TOP-REAL 2) ;
reconsider Q = rng g as non empty Subset of (TOP-REAL 2) ;
A2: I[01] is compact by HEINE:11, TOPMETR:27;
A3: TOP-REAL 2 is T_2 by SPPOL_1:26;
then consider f1 being Function of I[01] ,((TOP-REAL 2) | P) such that
A4: ( f = f1 & f1 is being_homeomorphism ) by A1, A2, Th64;
consider g1 being Function of I[01] ,((TOP-REAL 2) | Q) such that
A5: ( g = g1 & g1 is being_homeomorphism ) by A1, A2, A3, Th64;
reconsider p1 = f1 . O as Point of (TOP-REAL 2) by A1, A4;
reconsider p2 = f1 . I as Point of (TOP-REAL 2) by A1, A4;
reconsider q1 = g1 . O as Point of (TOP-REAL 2) by A1, A5;
reconsider q2 = g1 . I as Point of (TOP-REAL 2) by A1, A5;
A6: P is_an_arc_of p1,p2 by A1, A4, TOPREAL1:def 2;
A7: Q is_an_arc_of q1,q2 by A1, A5, TOPREAL1:def 2;
A8: for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in P implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) )
assume p in P ; :: thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )
then consider x being set such that
A9: ( x in dom f1 & p = f1 . x ) by A4, FUNCT_1:def 5;
thus ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A1, A4, A9; :: thesis: verum

end;

A10: for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in Q implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) )
assume p in Q ; :: thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )
then consider x being set such that
A11: ( x in dom g1 & p = g1 . x ) by A5, FUNCT_1:def 5;
thus ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A1, A4, A5, A11; :: thesis: verum

end;

A12: for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in P implies ( q1 `2 <= p `2 & p `2 <= q2 `2 ) )
assume p in P ; :: thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 )
then consider x being set such that
A13: ( x in dom f1 & p = f1 . x ) by A4, FUNCT_1:def 5;
thus ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A1, A4, A5, A13; :: thesis: verum

end;

for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in Q implies ( q1 `2 <= p `2 & p `2 <= q2 `2 ) )
assume p in Q ; :: thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 )
then consider x being set such that
A14: ( x in dom g1 & p = g1 . x ) by A5, FUNCT_1:def 5;
thus ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A1, A5, A14; :: thesis: verum

end;

hence rng f meets rng g by A6, A7, A8, A10, A12, Th62; :: thesis: verum