let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2)

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let C0 be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g )

assume that

A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and

A2: LE p1,p2,P and

A3: LE p2,p3,P and

A4: LE p3,p4,P ; :: 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 implies rng f meets rng g )

assume that

A5: ( f is continuous & f is one-to-one ) and

A6: ( g is continuous & g is one-to-one ) and

A7: C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } and

A8: f . 0 = p3 and

A9: f . 1 = p1 and

A10: g . 0 = p2 and

A11: g . 1 = p4 and

A12: rng f c= C0 and

A13: rng g c= C0 ; :: thesis: rng f meets rng g

A14: dom f = the carrier of I[01] by FUNCT_2:def 1;

A15: dom g = the carrier of I[01] by FUNCT_2:def 1;

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let C0 be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g )

assume that

A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and

A2: LE p1,p2,P and

A3: LE p2,p3,P and

A4: LE p3,p4,P ; :: 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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

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 & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 implies rng f meets rng g )

assume that

A5: ( f is continuous & f is one-to-one ) and

A6: ( g is continuous & g is one-to-one ) and

A7: C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } and

A8: f . 0 = p3 and

A9: f . 1 = p1 and

A10: g . 0 = p2 and

A11: g . 1 = p4 and

A12: rng f c= C0 and

A13: rng g c= C0 ; :: thesis: rng f meets rng g

A14: dom f = the carrier of I[01] by FUNCT_2:def 1;

A15: dom g = the carrier of I[01] by FUNCT_2:def 1;

per cases
( not p1 <> p2 or not p2 <> p3 or not p3 <> p4 or ( p1 <> p2 & p2 <> p3 & p3 <> p4 ) )
;

end;

suppose A16:
( not p1 <> p2 or not p2 <> p3 or not p3 <> p4 )
; :: thesis: rng f meets rng g

end;

now :: thesis: ( ( p1 = p2 & rng f meets rng g ) or ( p2 = p3 & rng f meets rng g ) or ( p3 = p4 & rng f meets rng g ) )end;

hence
rng f meets rng g
; :: thesis: verumper cases
( p1 = p2 or p2 = p3 or p3 = p4 )
by A16;

end;

case A17:
p1 = p2
; :: thesis: rng f meets rng g

A18:
p1 in rng f
by A9, A14, Lm14, BORSUK_1:40, FUNCT_1:def 3;

p2 in rng g by A10, A15, Lm13, BORSUK_1:40, FUNCT_1:def 3;

hence rng f meets rng g by A17, A18, XBOOLE_0:3; :: thesis: verum

end;p2 in rng g by A10, A15, Lm13, BORSUK_1:40, FUNCT_1:def 3;

hence rng f meets rng g by A17, A18, XBOOLE_0:3; :: thesis: verum

case A19:
p2 = p3
; :: thesis: rng f meets rng g

A20:
p3 in rng f
by A8, A14, Lm13, BORSUK_1:40, FUNCT_1:def 3;

p2 in rng g by A10, A15, Lm13, BORSUK_1:40, FUNCT_1:def 3;

hence rng f meets rng g by A19, A20, XBOOLE_0:3; :: thesis: verum

end;p2 in rng g by A10, A15, Lm13, BORSUK_1:40, FUNCT_1:def 3;

hence rng f meets rng g by A19, A20, XBOOLE_0:3; :: thesis: verum

case A21:
p3 = p4
; :: thesis: rng f meets rng g

A22:
p3 in rng f
by A8, A14, Lm13, BORSUK_1:40, FUNCT_1:def 3;

p4 in rng g by A11, A15, Lm14, BORSUK_1:40, FUNCT_1:def 3;

hence rng f meets rng g by A21, A22, XBOOLE_0:3; :: thesis: verum

end;p4 in rng g by A11, A15, Lm14, BORSUK_1:40, FUNCT_1:def 3;

hence rng f meets rng g by A21, A22, XBOOLE_0:3; :: thesis: verum

suppose
( p1 <> p2 & p2 <> p3 & p3 <> p4 )
; :: thesis: rng f meets rng g

then consider h being Function of (TOP-REAL 2),(TOP-REAL 2) such that

A23: h is being_homeomorphism and

A24: for q being Point of (TOP-REAL 2) holds |.(h . q).| = |.q.| and

A25: |[(- 1),0]| = h . p1 and

A26: |[0,1]| = h . p2 and

A27: |[1,0]| = h . p3 and

A28: |[0,(- 1)]| = h . p4 by A1, A2, A3, A4, JGRAPH_5:67;

A29: h is one-to-one by A23, TOPS_2:def 5;

reconsider f2 = h * f as Function of I[01],(TOP-REAL 2) ;

reconsider g2 = h * g as Function of I[01],(TOP-REAL 2) ;

A30: dom f2 = the carrier of I[01] by FUNCT_2:def 1;

A31: dom g2 = the carrier of I[01] by FUNCT_2:def 1;

A32: f2 . 1 = |[(- 1),0]| by A9, A25, A30, Lm14, BORSUK_1:40, FUNCT_1:12;

A33: g2 . 1 = |[0,(- 1)]| by A11, A28, A31, Lm14, BORSUK_1:40, FUNCT_1:12;

A34: f2 . 0 = |[1,0]| by A8, A27, A30, Lm13, BORSUK_1:40, FUNCT_1:12;

A35: g2 . 0 = |[0,1]| by A10, A26, A31, Lm13, BORSUK_1:40, FUNCT_1:12;

A36: ( f2 is continuous & f2 is one-to-one ) by A5, A23, JGRAPH_5:5, JGRAPH_5:6;

A37: ( g2 is continuous & g2 is one-to-one ) by A6, A23, JGRAPH_5:5, JGRAPH_5:6;

A38: rng f2 c= C0_{1}[ Point of (TOP-REAL 2)] means ( |.$1.| = 1 & $1 `2 <= $1 `1 & $1 `2 >= - ($1 `1) );

{ q1 where q1 is Point of (TOP-REAL 2) : S_{1}[q1] } is Subset of (TOP-REAL 2)
from JGRAPH_2:sch 1();

then reconsider KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } as Subset of (TOP-REAL 2) ;

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

{ q2 where q2 is Point of (TOP-REAL 2) : S_{2}[q2] } is Subset of (TOP-REAL 2)
from JGRAPH_2:sch 1();

then reconsider KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } as Subset of (TOP-REAL 2) ;

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

{ q3 where q3 is Point of (TOP-REAL 2) : S_{3}[q3] } is Subset of (TOP-REAL 2)
from JGRAPH_2:sch 1();

then reconsider KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } as Subset of (TOP-REAL 2) ;

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

{ q4 where q4 is Point of (TOP-REAL 2) : S_{4}[q4] } is Subset of (TOP-REAL 2)
from JGRAPH_2:sch 1();

then reconsider KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } as Subset of (TOP-REAL 2) ;

reconsider O = 0 , I = 1 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;

- (|[(- 1),0]| `1) = 1 by Lm4;

then A52: f2 . I in KXN by A32, Lm5, Lm12;

A53: f2 . O in KXP by A34, Lm6, Lm7, Lm12;

- (|[0,(- 1)]| `1) = 0 by Lm8;

then A54: g2 . I in KYN by A33, Lm9, Lm12;

- (|[0,1]| `1) = 0 by Lm10;

then g2 . O in KYP by A35, Lm11, Lm12;

then rng f2 meets rng g2 by A7, A36, A37, A38, A45, A52, A53, A54, Th14;

then consider x2 being object such that

A55: x2 in rng f2 and

A56: x2 in rng g2 by XBOOLE_0:3;

consider z2 being object such that

A57: z2 in dom f2 and

A58: x2 = f2 . z2 by A55, FUNCT_1:def 3;

consider z3 being object such that

A59: z3 in dom g2 and

A60: x2 = g2 . z3 by A56, FUNCT_1:def 3;

A61: dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

A62: g . z3 in rng g by A15, A59, FUNCT_1:def 3;

A63: f . z2 in rng f by A14, A57, FUNCT_1:def 3;

reconsider h1 = h as Function ;

A64: (h1 ") . x2 = (h1 ") . (h . (f . z2)) by A57, A58, FUNCT_1:12

.= f . z2 by A29, A61, A63, FUNCT_1:34 ;

A65: (h1 ") . x2 = (h1 ") . (h . (g . z3)) by A59, A60, FUNCT_1:12

.= g . z3 by A29, A61, A62, FUNCT_1:34 ;

A66: (h1 ") . x2 in rng f by A14, A57, A64, FUNCT_1:def 3;

(h1 ") . x2 in rng g by A15, A59, A65, FUNCT_1:def 3;

hence rng f meets rng g by A66, XBOOLE_0:3; :: thesis: verum

end;A23: h is being_homeomorphism and

A24: for q being Point of (TOP-REAL 2) holds |.(h . q).| = |.q.| and

A25: |[(- 1),0]| = h . p1 and

A26: |[0,1]| = h . p2 and

A27: |[1,0]| = h . p3 and

A28: |[0,(- 1)]| = h . p4 by A1, A2, A3, A4, JGRAPH_5:67;

A29: h is one-to-one by A23, TOPS_2:def 5;

reconsider f2 = h * f as Function of I[01],(TOP-REAL 2) ;

reconsider g2 = h * g as Function of I[01],(TOP-REAL 2) ;

A30: dom f2 = the carrier of I[01] by FUNCT_2:def 1;

A31: dom g2 = the carrier of I[01] by FUNCT_2:def 1;

A32: f2 . 1 = |[(- 1),0]| by A9, A25, A30, Lm14, BORSUK_1:40, FUNCT_1:12;

A33: g2 . 1 = |[0,(- 1)]| by A11, A28, A31, Lm14, BORSUK_1:40, FUNCT_1:12;

A34: f2 . 0 = |[1,0]| by A8, A27, A30, Lm13, BORSUK_1:40, FUNCT_1:12;

A35: g2 . 0 = |[0,1]| by A10, A26, A31, Lm13, BORSUK_1:40, FUNCT_1:12;

A36: ( f2 is continuous & f2 is one-to-one ) by A5, A23, JGRAPH_5:5, JGRAPH_5:6;

A37: ( g2 is continuous & g2 is one-to-one ) by A6, A23, JGRAPH_5:5, JGRAPH_5:6;

A38: rng f2 c= C0

proof

A45:
rng g2 c= C0
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f2 or y in C0 )

assume y in rng f2 ; :: thesis: y in C0

then consider x being object such that

A39: x in dom f2 and

A40: y = f2 . x by FUNCT_1:def 3;

A41: f2 . x = h . (f . x) by A39, FUNCT_1:12;

A42: f . x in rng f by A14, A39, FUNCT_1:def 3;

then A43: f . x in C0 by A12;

reconsider qf = f . x as Point of (TOP-REAL 2) by A42;

A44: ex q5 being Point of (TOP-REAL 2) st

( q5 = f . x & |.q5.| <= 1 ) by A7, A43;

|.(h . qf).| = |.qf.| by A24;

hence y in C0 by A7, A40, A41, A44; :: thesis: verum

end;assume y in rng f2 ; :: thesis: y in C0

then consider x being object such that

A39: x in dom f2 and

A40: y = f2 . x by FUNCT_1:def 3;

A41: f2 . x = h . (f . x) by A39, FUNCT_1:12;

A42: f . x in rng f by A14, A39, FUNCT_1:def 3;

then A43: f . x in C0 by A12;

reconsider qf = f . x as Point of (TOP-REAL 2) by A42;

A44: ex q5 being Point of (TOP-REAL 2) st

( q5 = f . x & |.q5.| <= 1 ) by A7, A43;

|.(h . qf).| = |.qf.| by A24;

hence y in C0 by A7, A40, A41, A44; :: thesis: verum

proof

defpred S
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g2 or y in C0 )

assume y in rng g2 ; :: thesis: y in C0

then consider x being object such that

A46: x in dom g2 and

A47: y = g2 . x by FUNCT_1:def 3;

A48: g2 . x = h . (g . x) by A46, FUNCT_1:12;

A49: g . x in rng g by A15, A46, FUNCT_1:def 3;

then A50: g . x in C0 by A13;

reconsider qg = g . x as Point of (TOP-REAL 2) by A49;

A51: ex q5 being Point of (TOP-REAL 2) st

( q5 = g . x & |.q5.| <= 1 ) by A7, A50;

|.(h . qg).| = |.qg.| by A24;

hence y in C0 by A7, A47, A48, A51; :: thesis: verum

end;assume y in rng g2 ; :: thesis: y in C0

then consider x being object such that

A46: x in dom g2 and

A47: y = g2 . x by FUNCT_1:def 3;

A48: g2 . x = h . (g . x) by A46, FUNCT_1:12;

A49: g . x in rng g by A15, A46, FUNCT_1:def 3;

then A50: g . x in C0 by A13;

reconsider qg = g . x as Point of (TOP-REAL 2) by A49;

A51: ex q5 being Point of (TOP-REAL 2) st

( q5 = g . x & |.q5.| <= 1 ) by A7, A50;

|.(h . qg).| = |.qg.| by A24;

hence y in C0 by A7, A47, A48, A51; :: thesis: verum

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

then reconsider KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } as Subset of (TOP-REAL 2) ;

defpred S

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

then reconsider KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } as Subset of (TOP-REAL 2) ;

defpred S

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

then reconsider KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } as Subset of (TOP-REAL 2) ;

defpred S

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

then reconsider KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } as Subset of (TOP-REAL 2) ;

reconsider O = 0 , I = 1 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;

- (|[(- 1),0]| `1) = 1 by Lm4;

then A52: f2 . I in KXN by A32, Lm5, Lm12;

A53: f2 . O in KXP by A34, Lm6, Lm7, Lm12;

- (|[0,(- 1)]| `1) = 0 by Lm8;

then A54: g2 . I in KYN by A33, Lm9, Lm12;

- (|[0,1]| `1) = 0 by Lm10;

then g2 . O in KYP by A35, Lm11, Lm12;

then rng f2 meets rng g2 by A7, A36, A37, A38, A45, A52, A53, A54, Th14;

then consider x2 being object such that

A55: x2 in rng f2 and

A56: x2 in rng g2 by XBOOLE_0:3;

consider z2 being object such that

A57: z2 in dom f2 and

A58: x2 = f2 . z2 by A55, FUNCT_1:def 3;

consider z3 being object such that

A59: z3 in dom g2 and

A60: x2 = g2 . z3 by A56, FUNCT_1:def 3;

A61: dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

A62: g . z3 in rng g by A15, A59, FUNCT_1:def 3;

A63: f . z2 in rng f by A14, A57, FUNCT_1:def 3;

reconsider h1 = h as Function ;

A64: (h1 ") . x2 = (h1 ") . (h . (f . z2)) by A57, A58, FUNCT_1:12

.= f . z2 by A29, A61, A63, FUNCT_1:34 ;

A65: (h1 ") . x2 = (h1 ") . (h . (g . z3)) by A59, A60, FUNCT_1:12

.= g . z3 by A29, A61, A62, FUNCT_1:34 ;

A66: (h1 ") . x2 in rng f by A14, A57, A64, FUNCT_1:def 3;

(h1 ") . x2 in rng g by A15, A59, A65, FUNCT_1:def 3;

hence rng f meets rng g by A66, XBOOLE_0:3; :: thesis: verum