let f, g be 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 & (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; 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]; ( 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 )
; 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 )
A16:
for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
A17:
for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
A18:
for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
P is_an_arc_of p1,p2
by A1, A11, TOPREAL1:def 1;
hence
rng f meets rng g
by A14, A15, A16, A18, A17, Th43; verum