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