let p1, p2, p3, p4 be Point of (); :: thesis: ( p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) implies for f, g being Function of I,() 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,() 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 non negative Real ;
reconsider P = circle (0,0,j) as non empty compact Subset of () ;
A2: P = { p6 where p6 is Point of () : |.p6.| = 1 } by Th24;
thus for f, g being Function of I,() 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,(); :: 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 that
A3: ( f is continuous & f is one-to-one ) and
A4: ( g is continuous & g is one-to-one ) and
A5: f . 0 = p1 and
A6: f . 1 = p3 and
A7: g . 0 = p2 and
A8: g . 1 = p4 and
A9: rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) and
A10: rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) ; :: thesis:
reconsider s = Sq_Circ as Function of (),() ;
A11: dom s = the carrier of () by FUNCT_2:def 1;
reconsider f1 = s * f as Function of I,() ;
reconsider g1 = s * g as Function of I,() ;
s is being_homeomorphism by JGRAPH_3:43;
then A12: s is continuous by TOPS_2:def 5;
A13: dom f = [.0,1.] by ;
then 0 in dom f by XXREAL_1:1;
then A14: f1 . 0 = Sq_Circ . p1 by ;
1 in dom f by ;
then A15: f1 . 1 = Sq_Circ . p3 by ;
A16: dom g = [.0,1.] by ;
then 0 in dom g by XXREAL_1:1;
then A17: g1 . 0 = Sq_Circ . p2 by ;
1 in dom g by ;
then A18: g1 . 1 = Sq_Circ . p4 by ;
defpred S1[ Point of ()] means |.\$1.| <= 1;
{ p8 where p8 is Point of () : S1[p8] } is Subset of () from then reconsider C0 = { p8 where p8 is Point of () : |.p8.| <= 1 } as Subset of () ;
A19: s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) = C0 by Th27;
A20: rng f1 c= C0
proof
let y be object ; :: 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 object such that
A21: x in dom f1 and
A22: y = f1 . x by FUNCT_1:def 3;
A23: x in dom f by ;
A24: f . x in dom s by ;
f . x in rng f by ;
then s . (f . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by ;
hence y in C0 by ; :: thesis: verum
end;
A25: rng g1 c= C0
proof
let y be object ; :: 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 object such that
A26: x in dom g1 and
A27: y = g1 . x by FUNCT_1:def 3;
A28: x in dom g by ;
A29: g . x in dom s by ;
g . x in rng g by ;
then s . (g . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by ;
hence y in C0 by ; :: thesis: verum
end;
reconsider q1 = s . p1, q2 = s . p2, q3 = s . p3, q4 = s . p4 as Point of () ;
q1,q2,q3,q4 are_in_this_order_on P by ;
then rng f1 meets rng g1 by A2, A3, A4, A12, A14, A15, A17, A18, A20, A25, Th18;
then consider y being object such that
A30: y in rng f1 and
A31: y in rng g1 by XBOOLE_0:3;
consider x1 being object such that
A32: x1 in dom f1 and
A33: y = f1 . x1 by ;
consider x2 being object such that
A34: x2 in dom g1 and
A35: y = g1 . x2 by ;
dom f1 c= dom f by RELAT_1:25;
then A36: f . x1 in rng f by ;
dom g1 c= dom g by RELAT_1:25;
then A37: g . x2 in rng g by ;
y = Sq_Circ . (f . x1) by ;
then A38: (Sq_Circ ") . y = f . x1 by ;
x1 in dom f by ;
then A39: f . x1 in rng f by FUNCT_1:def 3;
y = Sq_Circ . (g . x2) by ;
then A40: (Sq_Circ ") . y = g . x2 by ;
x2 in dom g by ;
then g . x2 in rng g by FUNCT_1:def 3;
hence rng f meets rng g by ; :: thesis: verum
end;