let A be SubSpace of T; :: thesis: A is T_2

per cases
( A is empty or not A is empty )
;

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 b_{1}, b_{2} being Element of bool the carrier of A st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} ) )

assume A2: not p = q ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of A st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

[#] 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 ; :: thesis: ex b_{1} being Element of bool the carrier of A st

( W9 is open & b_{1} is open & p in W9 & q in b_{1} & W9 misses b_{1} )

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 A1, A5, A6, XBOOLE_0:def 4; :: thesis: W9 misses V9

A9: W /\ V = {} by A7;

W9 /\ V9 = (W /\ (V /\ ([#] A))) /\ ([#] A) by XBOOLE_1:16

.= {} /\ ([#] A) by A9, XBOOLE_1:16

.= {} ;

hence W9 misses V9 ; :: thesis: verum

end;( b

assume A2: not p = q ; :: thesis: ex b

( b

[#] 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 ; :: thesis: ex b

( W9 is open & b

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 A1, A5, A6, XBOOLE_0:def 4; :: thesis: W9 misses V9

A9: W /\ V = {} by A7;

W9 /\ V9 = (W /\ (V /\ ([#] A))) /\ ([#] A) by XBOOLE_1:16

.= {} /\ ([#] A) by A9, XBOOLE_1:16

.= {} ;

hence W9 misses V9 ; :: thesis: verum