reconsider B = {(0. (TOP-REAL 2))} as Subset of (TOP-REAL 2) ;
A1:
B ` <> {}
by Th9;
reconsider W = B ` as non empty Subset of (TOP-REAL 2) by Th9;
defpred S1[ Point of (TOP-REAL 2)] means ( ( - 1 = $1 `1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( $1 `1 = 1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( - 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) or ( 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) );
A2: the carrier of ((TOP-REAL 2) | (B `)) =
[#] ((TOP-REAL 2) | (B `))
.=
B `
by PRE_TOPC:def 5
;
reconsider Kb = { q where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
let f, g be Function of I[01],(TOP-REAL 2); for K0 being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & (f . O) `1 = - 1 & (f . I) `1 = 1 & - 1 <= (f . O) `2 & (f . O) `2 <= 1 & - 1 <= (f . I) `2 & (f . I) `2 <= 1 & (g . O) `2 = - 1 & (g . I) `2 = 1 & - 1 <= (g . O) `1 & (g . O) `1 <= 1 & - 1 <= (g . I) `1 & (g . I) `1 <= 1 & rng f misses K0 & rng g misses K0 holds
rng f meets rng g
let K0 be Subset of (TOP-REAL 2); for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & (f . O) `1 = - 1 & (f . I) `1 = 1 & - 1 <= (f . O) `2 & (f . O) `2 <= 1 & - 1 <= (f . I) `2 & (f . I) `2 <= 1 & (g . O) `2 = - 1 & (g . I) `2 = 1 & - 1 <= (g . O) `1 & (g . O) `1 <= 1 & - 1 <= (g . I) `1 & (g . I) `1 <= 1 & rng f misses K0 & rng g misses K0 holds
rng f meets rng g
let O, I be Point of I[01]; ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & (f . O) `1 = - 1 & (f . I) `1 = 1 & - 1 <= (f . O) `2 & (f . O) `2 <= 1 & - 1 <= (f . I) `2 & (f . I) `2 <= 1 & (g . O) `2 = - 1 & (g . I) `2 = 1 & - 1 <= (g . O) `1 & (g . O) `1 <= 1 & - 1 <= (g . I) `1 & (g . I) `1 <= 1 & rng f misses K0 & rng g misses K0 implies rng f meets rng g )
A3:
dom f = the carrier of I[01]
by FUNCT_2:def 1;
assume A4:
( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & (f . O) `1 = - 1 & (f . I) `1 = 1 & - 1 <= (f . O) `2 & (f . O) `2 <= 1 & - 1 <= (f . I) `2 & (f . I) `2 <= 1 & (g . O) `2 = - 1 & (g . I) `2 = 1 & - 1 <= (g . O) `1 & (g . O) `1 <= 1 & - 1 <= (g . I) `1 & (g . I) `1 <= 1 & (rng f) /\ K0 = {} & (rng g) /\ K0 = {} )
; XBOOLE_0:def 7 rng f meets rng g
then consider h being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) such that
A5:
h is continuous
and
A6:
h is one-to-one
and
for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not h . t in K0 \/ Kb
and
A7:
for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
h . r in K0
and
A8:
for s being Point of (TOP-REAL 2) st s in Kb holds
h . s = s
by Th41;
rng f c= B `
then A11:
ex w being Function of I[01],(TOP-REAL 2) st
( w is continuous & w = h * f )
by A4, A5, A1, Th12;
then reconsider d1 = h * f as Function of I[01],(TOP-REAL 2) ;
the carrier of ((TOP-REAL 2) | W) <> {}
;
then A12:
dom h = the carrier of ((TOP-REAL 2) | (B `))
by FUNCT_2:def 1;
rng g c= B `
then A15:
ex w2 being Function of I[01],(TOP-REAL 2) st
( w2 is continuous & w2 = h * g )
by A4, A5, A1, Th12;
then reconsider d2 = h * g as Function of I[01],(TOP-REAL 2) ;
A16:
dom g = the carrier of I[01]
by FUNCT_2:def 1;
A17:
for r being Point of I[01] holds
( - 1 <= (d1 . r) `1 & (d1 . r) `1 <= 1 & - 1 <= (d2 . r) `1 & (d2 . r) `1 <= 1 & - 1 <= (d1 . r) `2 & (d1 . r) `2 <= 1 & - 1 <= (d2 . r) `2 & (d2 . r) `2 <= 1 )
f . I in Kb
by A4;
then
h . (f . I) = f . I
by A8;
then A30:
(d1 . I) `1 = 1
by A4, A3, FUNCT_1:13;
f . O in Kb
by A4;
then
h . (f . O) = f . O
by A8;
then A31:
(d1 . O) `1 = - 1
by A4, A3, FUNCT_1:13;
g . I in Kb
by A4;
then
h . (g . I) = g . I
by A8;
then A32:
(d2 . I) `2 = 1
by A4, A16, FUNCT_1:13;
g . O in Kb
by A4;
then
h . (g . O) = g . O
by A8;
then A33:
(d2 . O) `2 = - 1
by A4, A16, FUNCT_1:13;
set s = the Element of (rng d1) /\ (rng d2);
( d1 is one-to-one & d2 is one-to-one )
by A4, A6, FUNCT_1:24;
then
rng d1 meets rng d2
by A4, A11, A15, A31, A30, A33, A32, A17, JGRAPH_1:47;
then A34:
(rng d1) /\ (rng d2) <> {}
;
then
the Element of (rng d1) /\ (rng d2) in rng d1
by XBOOLE_0:def 4;
then consider t1 being object such that
A35:
t1 in dom d1
and
A36:
the Element of (rng d1) /\ (rng d2) = d1 . t1
by FUNCT_1:def 3;
A37:
f . t1 in rng f
by A3, A35, FUNCT_1:3;
the Element of (rng d1) /\ (rng d2) in rng d2
by A34, XBOOLE_0:def 4;
then consider t2 being object such that
A38:
t2 in dom d2
and
A39:
the Element of (rng d1) /\ (rng d2) = d2 . t2
by FUNCT_1:def 3;
h . (f . t1) = d1 . t1
by A35, FUNCT_1:12;
then A40:
h . (f . t1) = h . (g . t2)
by A36, A38, A39, FUNCT_1:12;
rng g c= the carrier of (TOP-REAL 2) \ B
then A43:
rng g c= the carrier of ((TOP-REAL 2) | (B `))
by A2, SUBSET_1:def 4;
dom g = the carrier of I[01]
by FUNCT_2:def 1;
then A44:
g . t2 in rng g
by A38, FUNCT_1:3;
rng f c= the carrier of (TOP-REAL 2) \ B
then
rng f c= the carrier of ((TOP-REAL 2) | (B `))
by A2, SUBSET_1:def 4;
then
f . t1 = g . t2
by A6, A43, A40, A12, A37, A44, FUNCT_1:def 4;
then
(rng f) /\ (rng g) <> {}
by A37, A44, XBOOLE_0:def 4;
hence
rng f meets rng g
; verum