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 b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A2: p <> q ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
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 b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & q in b1 & W misses b1 )
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