let A be SubSpace of T; :: thesis: A is Hausdorff
per cases
( A is empty or not A is empty )
;
suppose S:
not
A is
empty
;
:: thesis: A is Hausdorff let p,
q be
Point of
A;
:: according to PRE_TOPC:def 16 :: thesis: ( 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
;
:: thesis: 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 S;
then reconsider p' =
p,
q' =
q as
Point of
T by S, PRE_TOPC:55;
consider W,
V being
Subset of
T such that A3:
(
W is
open &
V is
open &
p' in W &
q' in V &
W misses V )
by A2, PRE_TOPC:def 16;
A4:
W /\ V = {}
by A3, XBOOLE_0:def 7;
reconsider W' =
W /\ ([#] A),
V' =
V /\ ([#] A) as
Subset of
A ;
take
W'
;
:: thesis: 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'
;
:: thesis: ( W' is open & V' is open & p in W' & q in V' & W' misses V' )
(
W in the
topology of
T &
V in the
topology of
T )
by A3, PRE_TOPC:def 5;
then
(
W' in the
topology of
A &
V' in the
topology of
A )
by PRE_TOPC:def 9;
hence
(
W' is
open &
V' is
open )
by PRE_TOPC:def 5;
:: thesis: ( p in W' & q in V' & W' misses V' )thus
(
p in W' &
q in V' )
by A3, S, XBOOLE_0:def 4;
:: thesis: W' misses V'W' /\ V' =
(W /\ (V /\ ([#] A))) /\ ([#] A)
by XBOOLE_1:16
.=
{} /\ ([#] A)
by A4, XBOOLE_1:16
.=
{}
;
hence
W' misses V'
by XBOOLE_0:def 7;
:: thesis: verum end;