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 non negative Real ;

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 Th24;

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

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 non negative Real ;

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 Th24;

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 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: rng f meets rng g

reconsider s = Sq_Circ as Function of (TOP-REAL 2),(TOP-REAL 2) ;

A11: 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:43;

then A12: s is continuous by TOPS_2:def 5;

A13: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;

then 0 in dom f by XXREAL_1:1;

then A14: f1 . 0 = Sq_Circ . p1 by A5, FUNCT_1:13;

1 in dom f by A13, XXREAL_1:1;

then A15: f1 . 1 = Sq_Circ . p3 by A6, FUNCT_1:13;

A16: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;

then 0 in dom g by XXREAL_1:1;

then A17: g1 . 0 = Sq_Circ . p2 by A7, FUNCT_1:13;

1 in dom g by A16, XXREAL_1:1;

then A18: g1 . 1 = Sq_Circ . p4 by A8, FUNCT_1:13;

defpred S_{1}[ Point of (TOP-REAL 2)] means |.$1.| <= 1;

{ p8 where p8 is Point of (TOP-REAL 2) : S_{1}[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) ;

A19: s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) = C0 by Th27;

A20: rng f1 c= C0

q1,q2,q3,q4 are_in_this_order_on P by A1, Th78;

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 A30, FUNCT_1:def 3;

consider x2 being object such that

A34: x2 in dom g1 and

A35: y = g1 . x2 by A31, FUNCT_1:def 3;

dom f1 c= dom f by RELAT_1:25;

then A36: f . x1 in rng f by A32, FUNCT_1:3;

dom g1 c= dom g by RELAT_1:25;

then A37: g . x2 in rng g by A34, FUNCT_1:3;

y = Sq_Circ . (f . x1) by A32, A33, FUNCT_1:12;

then A38: (Sq_Circ ") . y = f . x1 by A11, A36, FUNCT_1:32;

x1 in dom f by A32, FUNCT_1:11;

then A39: f . x1 in rng f by FUNCT_1:def 3;

y = Sq_Circ . (g . x2) by A34, A35, FUNCT_1:12;

then A40: (Sq_Circ ") . y = g . x2 by A11, A37, FUNCT_1:32;

x2 in dom g by A34, FUNCT_1:11;

then g . x2 in rng g by FUNCT_1:def 3;

hence rng f meets rng g by A38, A39, A40, XBOOLE_0:3; :: thesis: verum

end;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: rng f meets rng g

reconsider s = Sq_Circ as Function of (TOP-REAL 2),(TOP-REAL 2) ;

A11: 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:43;

then A12: s is continuous by TOPS_2:def 5;

A13: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;

then 0 in dom f by XXREAL_1:1;

then A14: f1 . 0 = Sq_Circ . p1 by A5, FUNCT_1:13;

1 in dom f by A13, XXREAL_1:1;

then A15: f1 . 1 = Sq_Circ . p3 by A6, FUNCT_1:13;

A16: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;

then 0 in dom g by XXREAL_1:1;

then A17: g1 . 0 = Sq_Circ . p2 by A7, FUNCT_1:13;

1 in dom g by A16, XXREAL_1:1;

then A18: g1 . 1 = Sq_Circ . p4 by A8, FUNCT_1:13;

defpred S

{ p8 where p8 is Point of (TOP-REAL 2) : S

then reconsider C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } as Subset of (TOP-REAL 2) ;

A19: s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) = C0 by Th27;

A20: rng f1 c= C0

proof

A25:
rng g1 c= C0
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 A21, FUNCT_1:11;

A24: f . x in dom s by A21, FUNCT_1:11;

f . x in rng f by A23, FUNCT_1:3;

then s . (f . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by A9, A24, FUNCT_1:def 6;

hence y in C0 by A19, A21, A22, FUNCT_1:12; :: thesis: verum

end;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 A21, FUNCT_1:11;

A24: f . x in dom s by A21, FUNCT_1:11;

f . x in rng f by A23, FUNCT_1:3;

then s . (f . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by A9, A24, FUNCT_1:def 6;

hence y in C0 by A19, A21, A22, FUNCT_1:12; :: thesis: verum

proof

reconsider q1 = s . p1, q2 = s . p2, q3 = s . p3, q4 = s . p4 as Point of (TOP-REAL 2) ;
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 A26, FUNCT_1:11;

A29: g . x in dom s by A26, FUNCT_1:11;

g . x in rng g by A28, FUNCT_1:3;

then s . (g . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by A10, A29, FUNCT_1:def 6;

hence y in C0 by A19, A26, A27, FUNCT_1:12; :: thesis: verum

end;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 A26, FUNCT_1:11;

A29: g . x in dom s by A26, FUNCT_1:11;

g . x in rng g by A28, FUNCT_1:3;

then s . (g . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by A10, A29, FUNCT_1:def 6;

hence y in C0 by A19, A26, A27, FUNCT_1:12; :: thesis: verum

q1,q2,q3,q4 are_in_this_order_on P by A1, Th78;

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 A30, FUNCT_1:def 3;

consider x2 being object such that

A34: x2 in dom g1 and

A35: y = g1 . x2 by A31, FUNCT_1:def 3;

dom f1 c= dom f by RELAT_1:25;

then A36: f . x1 in rng f by A32, FUNCT_1:3;

dom g1 c= dom g by RELAT_1:25;

then A37: g . x2 in rng g by A34, FUNCT_1:3;

y = Sq_Circ . (f . x1) by A32, A33, FUNCT_1:12;

then A38: (Sq_Circ ") . y = f . x1 by A11, A36, FUNCT_1:32;

x1 in dom f by A32, FUNCT_1:11;

then A39: f . x1 in rng f by FUNCT_1:def 3;

y = Sq_Circ . (g . x2) by A34, A35, FUNCT_1:12;

then A40: (Sq_Circ ") . y = g . x2 by A11, A37, FUNCT_1:32;

x2 in dom g by A34, FUNCT_1:11;

then g . x2 in rng g by FUNCT_1:def 3;

hence rng f meets rng g by A38, A39, A40, XBOOLE_0:3; :: thesis: verum