let f, g be Function of I[01],(TOP-REAL 2); :: thesis: 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 & (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; :: 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 that

A1: ( O = 0 & I = 1 ) and

A2: ( f is continuous & f is one-to-one ) and

A3: ( g is continuous & g is one-to-one ) and

A4: (f . O) `1 = a and

A5: (f . I) `1 = b and

A6: (g . O) `2 = c and

A7: (g . I) `2 = d and

A8: 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) ;

A9: I[01] is compact by HEINE:4, TOPMETR:20;

then consider f1 being Function of I[01],((TOP-REAL 2) | P) such that

A10: f = f1 and

A11: f1 is being_homeomorphism by A2, Th45;

reconsider Q = rng g as non empty Subset of (TOP-REAL 2) ;

consider g1 being Function of I[01],((TOP-REAL 2) | Q) such that

A12: g = g1 and

A13: g1 is being_homeomorphism by A3, A9, Th45;

reconsider q2 = g1 . I as Point of (TOP-REAL 2) by A7, A12;

reconsider q1 = g1 . O as Point of (TOP-REAL 2) by A6, A12;

A14: Q is_an_arc_of q1,q2 by A1, A13, TOPREAL1:def 1;

reconsider p2 = f1 . I as Point of (TOP-REAL 2) by A5, A10;

reconsider p1 = f1 . O as Point of (TOP-REAL 2) by A4, A10;

A15: for p being Point of (TOP-REAL 2) st p in P holds

( p1 `1 <= p `1 & p `1 <= p2 `1 )

( p1 `1 <= p `1 & p `1 <= p2 `1 )

( q1 `2 <= p `2 & p `2 <= q2 `2 )

( q1 `2 <= p `2 & p `2 <= q2 `2 )

hence rng f meets rng g by A14, A15, A16, A18, A17, Th43; :: thesis: verum

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; :: 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 that

A1: ( O = 0 & I = 1 ) and

A2: ( f is continuous & f is one-to-one ) and

A3: ( g is continuous & g is one-to-one ) and

A4: (f . O) `1 = a and

A5: (f . I) `1 = b and

A6: (g . O) `2 = c and

A7: (g . I) `2 = d and

A8: 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) ;

A9: I[01] is compact by HEINE:4, TOPMETR:20;

then consider f1 being Function of I[01],((TOP-REAL 2) | P) such that

A10: f = f1 and

A11: f1 is being_homeomorphism by A2, Th45;

reconsider Q = rng g as non empty Subset of (TOP-REAL 2) ;

consider g1 being Function of I[01],((TOP-REAL 2) | Q) such that

A12: g = g1 and

A13: g1 is being_homeomorphism by A3, A9, Th45;

reconsider q2 = g1 . I as Point of (TOP-REAL 2) by A7, A12;

reconsider q1 = g1 . O as Point of (TOP-REAL 2) by A6, A12;

A14: Q is_an_arc_of q1,q2 by A1, A13, TOPREAL1:def 1;

reconsider p2 = f1 . I as Point of (TOP-REAL 2) by A5, A10;

reconsider p1 = f1 . O as Point of (TOP-REAL 2) by A4, A10;

A15: for p being Point of (TOP-REAL 2) st p in P holds

( p1 `1 <= p `1 & p `1 <= p2 `1 )

proof

A16:
for p being Point of (TOP-REAL 2) st p in Q holds
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 ex x being object st

( x in dom f1 & p = f1 . x ) by A10, FUNCT_1:def 3;

hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A4, A5, A8, A10; :: thesis: verum

end;assume p in P ; :: thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )

then ex x being object st

( x in dom f1 & p = f1 . x ) by A10, FUNCT_1:def 3;

hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A4, A5, A8, A10; :: thesis: verum

( p1 `1 <= p `1 & p `1 <= p2 `1 )

proof

A17:
for p being Point of (TOP-REAL 2) st p in Q holds
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 ex x being object st

( x in dom g1 & p = g1 . x ) by A12, FUNCT_1:def 3;

hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A4, A5, A8, A10, A12; :: thesis: verum

end;assume p in Q ; :: thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )

then ex x being object st

( x in dom g1 & p = g1 . x ) by A12, FUNCT_1:def 3;

hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A4, A5, A8, A10, A12; :: thesis: verum

( q1 `2 <= p `2 & p `2 <= q2 `2 )

proof

A18:
for p being Point of (TOP-REAL 2) st p in P holds
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 ex x being object st

( x in dom g1 & p = g1 . x ) by A12, FUNCT_1:def 3;

hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A6, A7, A8, A12; :: thesis: verum

end;assume p in Q ; :: thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 )

then ex x being object st

( x in dom g1 & p = g1 . x ) by A12, FUNCT_1:def 3;

hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A6, A7, A8, A12; :: thesis: verum

( q1 `2 <= p `2 & p `2 <= q2 `2 )

proof

P is_an_arc_of p1,p2
by A1, A11, TOPREAL1:def 1;
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 ex x being object st

( x in dom f1 & p = f1 . x ) by A10, FUNCT_1:def 3;

hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A6, A7, A8, A10, A12; :: thesis: verum

end;assume p in P ; :: thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 )

then ex x being object st

( x in dom f1 & p = f1 . x ) by A10, FUNCT_1:def 3;

hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A6, A7, A8, A10, A12; :: thesis: verum

hence rng f meets rng g by A14, A15, A16, A18, A17, Th43; :: thesis: verum