let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: for C0 being Subset of (TOP-REAL 2) st C0 = { q where q is Point of (TOP-REAL 2) : |.q.| >= 1 } & f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = |[(- 1),0 ]| & f . 1 = |[1,0 ]| & g . 1 = |[0 ,1]| & g . 0 = |[0 ,(- 1)]| & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let C0 be Subset of (TOP-REAL 2); :: thesis: ( C0 = { q where q is Point of (TOP-REAL 2) : |.q.| >= 1 } & f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = |[(- 1),0 ]| & f . 1 = |[1,0 ]| & g . 1 = |[0 ,1]| & g . 0 = |[0 ,(- 1)]| & rng f c= C0 & rng g c= C0 implies rng f meets rng g )
assume A1:
( C0 = { q where q is Point of (TOP-REAL 2) : |.q.| >= 1 } & f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = |[(- 1),0 ]| & f . 1 = |[1,0 ]| & g . 1 = |[0 ,1]| & g . 0 = |[0 ,(- 1)]| & rng f c= C0 & rng g c= C0 )
; :: thesis: rng f meets rng g
defpred S1[ 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) : S1[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 S2[ 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) : S2[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 S3[ 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) : S3[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 S4[ 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) : S4[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 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
reconsider I = 1 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
A2:
( |[(- 1),0 ]| `1 = - 1 & |[(- 1),0 ]| `2 = 0 )
by EUCLID:56;
then A3: |.|[(- 1),0 ]|.| =
sqrt (((- 1) ^2 ) + (0 ^2 ))
by JGRAPH_3:10
.=
1
by SQUARE_1:83
;
|[(- 1),0 ]| `2 <= - (|[(- 1),0 ]| `1 )
by A2;
then A4:
f . O in KXN
by A1, A2, A3;
A5:
( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 )
by EUCLID:56;
then |.|[1,0 ]|.| =
sqrt ((1 ^2 ) + (0 ^2 ))
by JGRAPH_3:10
.=
1
by SQUARE_1:83
;
then A6:
f . I in KXP
by A1, A5;
A7:
( |[0 ,(- 1)]| `2 = - 1 & |[0 ,(- 1)]| `1 = 0 )
by EUCLID:56;
then A8: |.|[0 ,(- 1)]|.| =
sqrt ((0 ^2 ) + ((- 1) ^2 ))
by JGRAPH_3:10
.=
1
by SQUARE_1:83
;
|[0 ,(- 1)]| `2 <= - (|[0 ,(- 1)]| `1 )
by A7;
then A9:
g . O in KYN
by A1, A7, A8;
A10:
( |[0 ,1]| `2 = 1 & |[0 ,1]| `1 = 0 )
by EUCLID:56;
then A11: |.|[0 ,1]|.| =
sqrt ((0 ^2 ) + (1 ^2 ))
by JGRAPH_3:10
.=
1
by SQUARE_1:83
;
|[0 ,1]| `2 >= - (|[0 ,1]| `1 )
by A10;
then
g . I in KYP
by A1, A10, A11;
hence
rng f meets rng g
by A1, A4, A6, A9, Th17; :: thesis: verum