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_1 then A1:
not the
carrier of
[:T1,T2:] is
empty
;
let p,
q be
Point of
[:T1,T2:];
URYSOHN1:def 7 ( 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 & not q in b1 & q in b2 & not p in 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 & not q in b1 & q in b2 & not p in 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 & not q in b1 & q in b2 & not p in b2 )then consider Y,
V being
Subset of
T1 such that A9:
(
Y is
open &
V is
open )
and A10:
x in Y
and A11:
not
z in Y
and A12:
z in V
and A13:
not
x in V
by URYSOHN1:def 7;
set X =
[:Y,([#] T2):];
set Z =
[:V,([#] T2):];
A14:
( not
q in [:Y,([#] T2):] & not
p in [:V,([#] T2):] )
by A8, A5, A11, A13, ZFMISC_1:87;
A15:
(
[:Y,([#] T2):] is
open &
[:V,([#] T2):] is
open )
by A9, BORSUK_1:6;
(
p in [:Y,([#] T2):] &
q in [:V,([#] T2):] )
by A7, A8, A4, A5, A10, A12, 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 & not
q in b1 &
q in b2 & not
p in b2 )
by A15, A14;
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 & not q in b1 & q in b2 & not p in b2 )then consider Y,
V being
Subset of
T2 such that A16:
(
Y is
open &
V is
open )
and A17:
y in Y
and A18:
not
v in Y
and A19:
v in V
and A20:
not
y in V
by A2, A8, A5, URYSOHN1:def 7;
reconsider Y =
Y,
V =
V as
Subset of
T2 ;
set X =
[:([#] T1),Y:];
set Z =
[:([#] T1),V:];
A21:
( not
p in [:([#] T1),V:] & not
q in [:([#] T1),Y:] )
by A8, A5, A18, A20, ZFMISC_1:87;
A22:
(
[:([#] T1),Y:] is
open &
[:([#] T1),V:] is
open )
by A16, BORSUK_1:6;
(
p in [:([#] T1),Y:] &
q in [:([#] T1),V:] )
by A6, A8, A3, A5, A17, A19, 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 & not
q in b1 &
q in b2 & not
p in b2 )
by A22, A21;
verum end; end;