let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for C0 being Subset of (TOP-REAL 2) st C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & |.p1.| = 1 & |.p2.| = 1 & |.p3.| = 1 & |.p4.| = 1 & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h is being_homeomorphism & h .: C0 c= C0 & h . p1 = |[(- 1),0]| & h . p2 = |[0,1]| & h . p3 = |[1,0]| & h . p4 = |[0,(- 1)]| ) holds
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let C0 be Subset of (TOP-REAL 2); :: thesis: ( C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & |.p1.| = 1 & |.p2.| = 1 & |.p3.| = 1 & |.p4.| = 1 & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h is being_homeomorphism & h .: C0 c= C0 & h . p1 = |[(- 1),0]| & h . p2 = |[0,1]| & h . p3 = |[1,0]| & h . p4 = |[0,(- 1)]| ) implies for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g )
assume A1: ( C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & |.p1.| = 1 & |.p2.| = 1 & |.p3.| = 1 & |.p4.| = 1 & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h is being_homeomorphism & h .: C0 c= C0 & h . p1 = |[(- 1),0]| & h . p2 = |[0,1]| & h . p3 = |[1,0]| & h . p4 = |[0,(- 1)]| ) ) ; :: thesis: for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
then consider h being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A2: h is being_homeomorphism and
A3: h .: C0 c= C0 and
A4: h . p1 = |[(- 1),0]| and
A5: h . p2 = |[0,1]| and
A6: h . p3 = |[1,0]| and
A7: h . p4 = |[0,(- 1)]| ;
let f, g be Function of I[01],(TOP-REAL 2); :: thesis: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 implies rng f meets rng g )
assume that
A8: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one ) and
A9: f . 0 = p1 and
A10: f . 1 = p3 and
A11: g . 0 = p4 and
A12: g . 1 = p2 and
A13: rng f c= C0 and
A14: rng g c= C0 ; :: thesis: rng f meets rng g
reconsider f2 = h * f as Function of I[01],(TOP-REAL 2) ;
0 in dom f2 by Lm1, BORSUK_1:40, FUNCT_2:def 1;
then A15: f2 . 0 = |[(- 1),0]| by A4, A9, FUNCT_1:12;
reconsider g2 = h * g as Function of I[01],(TOP-REAL 2) ;
0 in dom g2 by Lm1, BORSUK_1:40, FUNCT_2:def 1;
then A16: g2 . 0 = |[0,(- 1)]| by A7, A11, FUNCT_1:12;
1 in dom g2 by Lm2, BORSUK_1:40, FUNCT_2:def 1;
then A17: g2 . 1 = |[0,1]| by A5, A12, FUNCT_1:12;
A18: rng f2 c= C0

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f2 or y in C0 )
A19: dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
assume y in rng f2 ; :: thesis: y in C0
then consider x being object such that
A20: x in dom f2 and
A21: y = f2 . x by FUNCT_1:def 3;
x in dom f by A20, FUNCT_1:11;
then A22: f . x in rng f by FUNCT_1:def 3;
y = h . (f . x) by A20, A21, FUNCT_1:12;
then y in h .: C0 by A13, A22, A19, FUNCT_1:def 6;
hence y in C0 by A3; :: thesis: verum

end;

A23: rng g2 c= C0

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g2 or y in C0 )
A24: dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
assume y in rng g2 ; :: thesis: y in C0
then consider x being object such that
A25: x in dom g2 and
A26: y = g2 . x by FUNCT_1:def 3;
x in dom g by A25, FUNCT_1:11;
then A27: g . x in rng g by FUNCT_1:def 3;
y = h . (g . x) by A25, A26, FUNCT_1:12;
then y in h .: C0 by A14, A27, A24, FUNCT_1:def 6;
hence y in C0 by A3; :: thesis: verum

end;

1 in dom f2 by Lm2, BORSUK_1:40, FUNCT_2:def 1;
then A28: f2 . 1 = |[1,0]| by A6, A10, FUNCT_1:12;
( h is continuous & h is one-to-one ) by A2, TOPS_2:def 5;
then rng f2 meets rng g2 by A1, A8, A15, A28, A16, A17, A18, A23, Th16;
then consider q5 being object such that
A29: q5 in rng f2 and
A30: q5 in rng g2 by XBOOLE_0:3;
consider x being object such that
A31: x in dom f2 and
A32: q5 = f2 . x by A29, FUNCT_1:def 3;
x in dom f by A31, FUNCT_1:11;
then A33: f . x in rng f by FUNCT_1:def 3;
consider u being object such that
A34: u in dom g2 and
A35: q5 = g2 . u by A30, FUNCT_1:def 3;
A36: ( q5 = h . (g . u) & g . u in dom h ) by A34, A35, FUNCT_1:11, FUNCT_1:12;
A37: h is one-to-one by A2, TOPS_2:def 5;
u in dom g by A34, FUNCT_1:11;
then A38: g . u in rng g by FUNCT_1:def 3;
( q5 = h . (f . x) & f . x in dom h ) by A31, A32, FUNCT_1:11, FUNCT_1:12;
then f . x = g . u by A37, A36, FUNCT_1:def 4;
hence rng f meets rng g by A33, A38, XBOOLE_0:3; :: thesis: verum