let T be TopSpace; :: thesis: ( T is T_3 implies T is T_2 )
assume A1: T is T_3 ; :: thesis: T is T_2
let p, q be Point of T; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A2: p <> q ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
then A3: not p in {q} by TARSKI:def 1;

now :: thesis: not the carrier of T = {}

assume A4: the carrier of T = {} ; :: thesis: contradiction
then p = {} by SUBSET_1:def 1;
hence contradiction by A2, A4, SUBSET_1:def 1; :: thesis: verum

end;

then reconsider T9 = T as non empty TopSpace ;
reconsider p = p, q = q as Point of T9 ;
p in {q} ` by A3, SUBSET_1:29;
then consider W, V being Subset of T such that
A5: ( W is open & V is open & p in W & {q} c= V & W misses V ) by A1, COMPTS_1:def 2;
take W ; :: thesis: ex b₁ being Element of bool the carrier of T st
( W is open & b₁ is open & p in W & q in b₁ & W misses b₁ )
take V ; :: thesis: ( W is open & V is open & p in W & q in V & W misses V )
q in {q} by TARSKI:def 1;
hence ( W is open & V is open & p in W & q in V & W misses V ) by A5; :: thesis: verum