let T be non empty TopSpace; :: thesis: for A being non empty SubSpace of T st T is T_2 holds
A is T_2

let A be non empty SubSpace of T; :: thesis: ( T is T_2 implies A is T_2 )
assume A1: T is T_2 ; :: thesis: A is T_2
for p, q being Point of A st not p = q holds
ex W, V being Subset of A st
( W is open & V is open & p in W & q in V & W misses V )
proof
let p, q be Point of A; :: thesis: ( not p = q implies ex W, V being Subset of A st
( W is open & V is open & p in W & q in V & W misses V ) )

assume A2: not p = q ; :: thesis: ex W, V being Subset of A st
( W is open & V is open & p in W & q in V & W misses V )

reconsider p9 = p, q9 = q as Point of T by 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 & q9 in V ) and
A6: W misses V by A1, A2;
reconsider W9 = W /\ ([#] A), V9 = V /\ ([#] A) as Subset of A ;
V in the topology of T by A4;
then A7: V9 in the topology of A by PRE_TOPC:def 4;
take W9 ; :: thesis: ex V being Subset of A st
( W9 is open & V is open & p in W9 & q in V & W9 misses V )

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 A7; :: thesis: ( p in W9 & q in V9 & W9 misses V9 )
thus ( p in W9 & q in V9 ) by ; :: thesis: W9 misses V9
A8: W /\ V = {} by ;
W9 /\ V9 = (W /\ (V /\ ([#] A))) /\ ([#] A) by XBOOLE_1:16
.= {} /\ ([#] A) by
.= {} ;
hence W9 misses V9 by XBOOLE_0:def 7; :: thesis: verum
end;
hence A is T_2 ; :: thesis: verum