let A be SubSpace of T; :: thesis: A is T_2
per cases ( A is empty or not A is empty ) ;
suppose A is empty ; :: thesis: A is T_2
end;
suppose A1: not A is empty ; :: thesis: A is T_2
let p, q be Point of A; :: according to PRE_TOPC:def 10 :: 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 4;
then not T is empty by A1;
then reconsider p9 = p, q9 = q as Point of T by ;
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 ;
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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( p in W9 & q in V9 & W9 misses V9 )
thus ( p in W9 & q in V9 ) by ; :: thesis: W9 misses V9
A9: W /\ V = {} by A7;
W9 /\ V9 = (W /\ (V /\ ([#] A))) /\ ([#] A) by XBOOLE_1:16
.= {} /\ ([#] A) by
.= {} ;
hence W9 misses V9 ; :: thesis: verum
end;
end;