let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: ( p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),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 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle (- 1),1,(- 1),1 & rng g c= closed_inside_of_rectangle (- 1),1,(- 1),1 holds
rng f meets rng g )
set K = rectangle (- 1),1,(- 1),1;
set K0 = closed_inside_of_rectangle (- 1),1,(- 1),1;
assume A1: p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),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 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle (- 1),1,(- 1),1 & rng g c= closed_inside_of_rectangle (- 1),1,(- 1),1 holds
rng f meets rng g
reconsider j = 1 as real non negative number ;
reconsider P = circle 0 ,0 ,j as non empty compact Subset of (TOP-REAL 2) ;
A2: P = { p6 where p6 is Point of (TOP-REAL 2) : |.p6.| = 1 } by Th33;
thus 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 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle (- 1),1,(- 1),1 & rng g c= closed_inside_of_rectangle (- 1),1,(- 1),1 holds
rng f meets rng g :: thesis: verum

proof

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 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle (- 1),1,(- 1),1 & rng g c= closed_inside_of_rectangle (- 1),1,(- 1),1 implies rng f meets rng g )
assume A3: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle (- 1),1,(- 1),1 & rng g c= closed_inside_of_rectangle (- 1),1,(- 1),1 ) ; :: thesis: rng f meets rng g
reconsider s = Sq_Circ as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A4: dom s = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
reconsider f1 = s * f as Function of I[01] ,(TOP-REAL 2) ;
reconsider g1 = s * g as Function of I[01] ,(TOP-REAL 2) ;
s is being_homeomorphism by JGRAPH_3:54;
then A5: s is continuous by TOPS_2:def 5;
then A6: f1 is continuous by A3;
A7: g1 is continuous by A3, A5;
A8: f1 is one-to-one by A3, FUNCT_1:46;
A9: g1 is one-to-one by A3, FUNCT_1:46;
A10: dom f = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then 0 in dom f by XXREAL_1:1;
then A11: f1 . 0 = Sq_Circ . p1 by A3, FUNCT_1:23;
1 in dom f by A10, XXREAL_1:1;
then A12: f1 . 1 = Sq_Circ . p3 by A3, FUNCT_1:23;
A13: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
then 0 in dom g by XXREAL_1:1;
then A14: g1 . 0 = Sq_Circ . p2 by A3, FUNCT_1:23;
1 in dom g by A13, XXREAL_1:1;
then A15: g1 . 1 = Sq_Circ . p4 by A3, FUNCT_1:23;
defpred S₁[ Point of (TOP-REAL 2)] means |.$1.| <= 1;
{ p8 where p8 is Point of (TOP-REAL 2) : S₁[p8] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
then reconsider C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } as Subset of (TOP-REAL 2) ;
A16: s .: (closed_inside_of_rectangle (- 1),1,(- 1),1) = C0 by Th36;
A17: rng f1 c= C0

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f1 or y in C0 )
assume y in rng f1 ; :: thesis: y in C0
then consider x being set such that
A18: ( x in dom f1 & y = f1 . x ) by FUNCT_1:def 5;
A19: ( x in dom f & f . x in dom s ) by A18, FUNCT_1:21;
then f . x in rng f by FUNCT_1:12;
then s . (f . x) in s .: (closed_inside_of_rectangle (- 1),1,(- 1),1) by A3, A19, FUNCT_1:def 12;
hence y in C0 by A16, A18, FUNCT_1:22; :: thesis: verum

end;

A20: rng g1 c= C0

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g1 or y in C0 )
assume y in rng g1 ; :: thesis: y in C0
then consider x being set such that
A21: ( x in dom g1 & y = g1 . x ) by FUNCT_1:def 5;
A22: ( x in dom g & g . x in dom s ) by A21, FUNCT_1:21;
then g . x in rng g by FUNCT_1:12;
then s . (g . x) in s .: (closed_inside_of_rectangle (- 1),1,(- 1),1) by A3, A22, FUNCT_1:def 12;
hence y in C0 by A16, A21, FUNCT_1:22; :: thesis: verum

end;

reconsider q1 = s . p1, q2 = s . p2, q3 = s . p3, q4 = s . p4 as Point of (TOP-REAL 2) ;
q1,q2,q3,q4 are_in_this_order_on P by A1, Th88;
then rng f1 meets rng g1 by A2, A6, A7, A8, A9, A11, A12, A14, A15, A17, A20, Th27;
then consider y being set such that
A23: ( y in rng f1 & y in rng g1 ) by XBOOLE_0:3;
consider x1 being set such that
A24: ( x1 in dom f1 & y = f1 . x1 ) by A23, FUNCT_1:def 5;
consider x2 being set such that
A25: ( x2 in dom g1 & y = g1 . x2 ) by A23, FUNCT_1:def 5;
dom f1 c= dom f by RELAT_1:44;
then A26: f . x1 in rng f by A24, FUNCT_1:12;
dom g1 c= dom g by RELAT_1:44;
then A27: g . x2 in rng g by A25, FUNCT_1:12;
y = Sq_Circ . (f . x1) by A24, FUNCT_1:22;
then A28: (Sq_Circ " ) . y = f . x1 by A4, A26, FUNCT_1:54;
x1 in dom f by A24, FUNCT_1:21;
then A29: f . x1 in rng f by FUNCT_1:def 5;
y = Sq_Circ . (g . x2) by A25, FUNCT_1:22;
then A30: (Sq_Circ " ) . y = g . x2 by A4, A27, FUNCT_1:54;
x2 in dom g by A25, FUNCT_1:21;
then g . x2 in rng g by FUNCT_1:def 5;
hence rng f meets rng g by A28, A29, A30, XBOOLE_0:3; :: thesis: verum

end;