let T be non empty discrete TopSpace; :: 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 A1: not 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₂ )
take W = {p}; :: 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 = {q}; :: thesis: ( W is open & V is open & p in W & q in V & W misses V )
thus ( W is open & V is open ) by TDLAT_3:15; :: thesis: ( p in W & q in V & W misses V )
W /\ V c= {}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in W /\ V or a in {} )
assume A2: a in W /\ V ; :: thesis: a in {}
then a in W by XBOOLE_0:def 4;
then A3: a = p by TARSKI:def 1;
assume not a in {} ; :: thesis: contradiction
a in V by A2, XBOOLE_0:def 4;
hence contradiction by A1, A3, TARSKI:def 1; :: thesis: verum

end;

hence ( p in W & q in V & W /\ V = {} ) by TARSKI:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum