let A be SubSpace of T; A is T_2
per cases
( A is empty or not A is empty )
;
suppose A1:
not
A is
empty
;
A is T_2 let p,
q be
Point of
A;
PRE_TOPC:def 10 ( 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 4;
then
not
T is
empty
by A1;
then reconsider p9 =
p,
q9 =
q as
Point of
T by A1, PRE_TOPC:25;
consider W,
V being
Subset of
T such that A3:
W is
open
and A4:
V is
open
and A5:
p9 in W
and A6:
q9 in V
and A7:
W misses V
by A2, PRE_TOPC:def 10;
reconsider W9 =
W /\ ([#] A),
V9 =
V /\ ([#] A) as
Subset of
A ;
V in the
topology of
T
by A4;
then A8:
V9 in the
topology of
A
by PRE_TOPC:def 4;
take
W9
;
ex b1 being Element of bool the carrier of A st
( W9 is open & b1 is open & p in W9 & q in b1 & W9 misses b1 )take
V9
;
( W9 is open & V9 is open & p in W9 & q in V9 & W9 misses V9 )
W in the
topology of
T
by A3;
then
W9 in the
topology of
A
by PRE_TOPC:def 4;
hence
(
W9 is
open &
V9 is
open )
by A8;
( p in W9 & q in V9 & W9 misses V9 )thus
(
p in W9 &
q in V9 )
by A1, A5, A6, XBOOLE_0:def 4;
W9 misses V9A9:
W /\ V = {}
by A7;
W9 /\ V9 =
(W /\ (V /\ ([#] A))) /\ ([#] A)
by XBOOLE_1:16
.=
{} /\ ([#] A)
by A9, XBOOLE_1:16
.=
{}
;
hence
W9 misses V9
;
verum end;