let A be SubSpace of T; A is Hausdorff
per cases
( A is empty or not A is empty )
;
suppose A1:
not
A is
empty
;
A is Hausdorff let p,
q be
Point of ;
PRE_TOPC:def 16 ( p = q or ex b1, b2 being Element of bool the carrier of A st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )assume A2:
not
p = q
;
ex b1, b2 being Element of bool the carrier of A st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
[#] A c= [#] T
by PRE_TOPC:def 9;
then
not
T is
empty
by A1;
then reconsider p' =
p,
q' =
q as
Point of
by A1, PRE_TOPC:55;
consider W,
V being
Subset of
such that A3:
W is
open
and A4:
V is
open
and A5:
p' in W
and A6:
q' in V
and A7:
W misses V
by A2, PRE_TOPC:def 16;
reconsider W' =
W /\ ([#] A),
V' =
V /\ ([#] A) as
Subset of ;
V in the
topology of
T
by A4, PRE_TOPC:def 5;
then A8:
V' in the
topology of
A
by PRE_TOPC:def 9;
take
W'
;
ex b1 being Element of bool the carrier of A st
( W' is open & b1 is open & p in W' & q in b1 & W' misses b1 )take
V'
;
( W' is open & V' is open & p in W' & q in V' & W' misses V' )
W in the
topology of
T
by A3, PRE_TOPC:def 5;
then
W' in the
topology of
A
by PRE_TOPC:def 9;
hence
(
W' is
open &
V' is
open )
by A8, PRE_TOPC:def 5;
( p in W' & q in V' & W' misses V' )thus
(
p in W' &
q in V' )
by A1, A5, A6, XBOOLE_0:def 4;
W' misses V'A9:
W /\ V = {}
by A7, XBOOLE_0:def 7;
W' /\ V' =
(W /\ (V /\ ([#] A))) /\ ([#] A)
by XBOOLE_1:16
.=
{} /\ ([#] A)
by A9, XBOOLE_1:16
.=
{}
;
hence
W' misses V'
by XBOOLE_0:def 7;
verum end;