let T be non empty discrete TopSpace; :: thesis: T is regular
let p be Point of T; :: according to COMPTS_1:def 2 :: thesis: for b₁ being Element of bool the carrier of T holds
( b₁ = {} or not b₁ is closed or not p in b₁ ` or ex b<sub>2</sub>, b<sub>3</sub> being Element of bool the carrier of T st
( b<sub>2</sub> is open & b<sub>3</sub> is open & p in b<sub>2</sub> & b<sub>1</sub> c= b<sub>3</sub> & b<sub>2</sub> misses b<sub>3</sub> ) )
let P be Subset of T; :: thesis: ( P = {} or not P is closed or not p in P ` or ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & P c= b₂ & b₁ misses b₂ ) )
assume that
P <> {} and
P is closed and
A1: p in P ` ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & P c= 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 & P c= b₁ & W misses b₁ )
take V = P; :: thesis: ( W is open & V is open & p in W & P c= V & W misses V )
thus ( W is open & V is open ) by TDLAT_3:15; :: thesis: ( p in W & P c= V & W misses V )
A2: not p in P by A1, XBOOLE_0:def 5;
W /\ V c= {}

proof

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

end;

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