reconsider I = 1 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;
reconsider O = 0 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;
defpred S1[ Point of (TOP-REAL 2)] means ( |.$1.| = 1 & $1 `2 <= $1 `1 & $1 `2 >= - ($1 `1) );
let f, g be Function of I[01],(TOP-REAL 2); 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); ( 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 )
; rng f meets rng g
{ 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) ;
A2:
|[0,1]| `1 = 0
by EUCLID:52;
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) ;
A3:
|[0,(- 1)]| `1 = 0
by EUCLID:52;
|[0,(- 1)]| `2 = - 1
by EUCLID:52;
then A4: |.|[0,(- 1)]|.| =
sqrt ((0 ^2) + ((- 1) ^2))
by A3, JGRAPH_3:1
.=
1
by SQUARE_1:18
;
|[0,(- 1)]| `2 <= - (|[0,(- 1)]| `1)
by A3, EUCLID:52;
then A5:
g . O in KYN
by A1, A3, A4;
A6:
|[(- 1),0]| `1 = - 1
by EUCLID:52;
then A7:
|[(- 1),0]| `2 <= - (|[(- 1),0]| `1)
by EUCLID:52;
|[0,1]| `2 = 1
by EUCLID:52;
then A8: |.|[0,1]|.| =
sqrt ((0 ^2) + (1 ^2))
by A2, JGRAPH_3:1
.=
1
by SQUARE_1:18
;
|[0,1]| `2 >= - (|[0,1]| `1)
by A2, EUCLID:52;
then A9:
g . I in KYP
by A1, A2, A8;
A10:
( |[1,0]| `1 = 1 & |[1,0]| `2 = 0 )
by EUCLID:52;
then |.|[1,0]|.| =
sqrt ((1 ^2) + (0 ^2))
by JGRAPH_3:1
.=
1
by SQUARE_1:18
;
then A11:
f . I in KXP
by A1, A10;
A12:
|[(- 1),0]| `2 = 0
by EUCLID:52;
then |.|[(- 1),0]|.| =
sqrt (((- 1) ^2) + (0 ^2))
by A6, JGRAPH_3:1
.=
1
by SQUARE_1:18
;
then
f . O in KXN
by A1, A6, A12, A7;
hence
rng f meets rng g
by A1, A11, A5, A9, Th14; verum