set T = [:T1,T2:];
per cases
( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) )
;
suppose
( not
T1 is
empty & not
T2 is
empty )
;
[:T1,T2:] is T_2 then A1:
not the
carrier of
[:T1,T2:] is
empty
;
let p,
q be
Point of
[:T1,T2:];
PRE_TOPC:def 10 ( p = q or ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )assume A2:
p <> q
;
ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
q in the
carrier of
[:T1,T2:]
by A1;
then
q in [: the carrier of T1, the carrier of T2:]
by BORSUK_1:def 2;
then consider z,
v being
object such that A3:
z in the
carrier of
T1
and A4:
v in the
carrier of
T2
and A5:
q = [z,v]
by ZFMISC_1:def 2;
p in the
carrier of
[:T1,T2:]
by A1;
then
p in [: the carrier of T1, the carrier of T2:]
by BORSUK_1:def 2;
then consider x,
y being
object such that A6:
x in the
carrier of
T1
and A7:
y in the
carrier of
T2
and A8:
p = [x,y]
by ZFMISC_1:def 2;
reconsider y =
y,
v =
v as
Point of
T2 by A7, A4;
reconsider x =
x,
z =
z as
Point of
T1 by A6, A3;
per cases
( x <> z or x = z )
;
suppose
x <> z
;
ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )then consider Y,
V being
Subset of
T1 such that A9:
(
Y is
open &
V is
open )
and A10:
(
x in Y &
z in V )
and A11:
Y misses V
by PRE_TOPC:def 10;
reconsider Y =
Y,
V =
V as
Subset of
T1 ;
reconsider X =
[:Y,([#] T2):],
Z =
[:V,([#] T2):] as
Subset of
[:T1,T2:] ;
A12:
X misses Z
by A11, ZFMISC_1:104;
A13:
(
X is
open &
Z is
open )
by A9, BORSUK_1:6;
(
p in X &
q in Z )
by A7, A8, A4, A5, A10, ZFMISC_1:87;
hence
ex
b1,
b2 being
Element of
bool the
carrier of
[:T1,T2:] st
(
b1 is
open &
b2 is
open &
p in b1 &
q in b2 &
b1 misses b2 )
by A13, A12;
verum end; suppose
x = z
;
ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )then consider Y,
V being
Subset of
T2 such that A14:
(
Y is
open &
V is
open )
and A15:
(
y in Y &
v in V )
and A16:
Y misses V
by A2, A8, A5, PRE_TOPC:def 10;
reconsider Y =
Y,
V =
V as
Subset of
T2 ;
reconsider X =
[:([#] T1),Y:],
Z =
[:([#] T1),V:] as
Subset of
[:T1,T2:] ;
A17:
X misses Z
by A16, ZFMISC_1:104;
A18:
(
X is
open &
Z is
open )
by A14, BORSUK_1:6;
(
p in X &
q in Z )
by A6, A8, A3, A5, A15, ZFMISC_1:87;
hence
ex
b1,
b2 being
Element of
bool the
carrier of
[:T1,T2:] st
(
b1 is
open &
b2 is
open &
p in b1 &
q in b2 &
b1 misses b2 )
by A18, A17;
verum end; end;