let T be non empty TopSpace; :: thesis: ( T is T_4 implies T is regular )
assume A1: T is T_4 ; :: 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
A2: ( P <> {} & P is closed ) and
A3: 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₂ )
A4: not p in P by A3, XBOOLE_0:def 5;
P /\ {p} c= {}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P /\ {p} or a in {} )
assume A5: a in P /\ {p} ; :: thesis: a in {}
assume not a in {} ; :: thesis: contradiction
( a in P & a in {p} ) by A5, XBOOLE_0:def 4;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum

end;

then P /\ {p} = {} ;
then P misses {p} ;
then consider R, Q being Subset of T such that
A6: ( R is open & Q is open & {p} c= R & P c= Q & R misses Q ) by A1, A2, COMPTS_1:def 3;
take R ; :: thesis: ex b₁ being Element of bool the carrier of T st
( R is open & b₁ is open & p in R & P c= b₁ & R misses b₁ )
take Q ; :: thesis: ( R is open & Q is open & p in R & P c= Q & R misses Q )
p in {p} by TARSKI:def 1;
hence ( R is open & Q is open & p in R & P c= Q & R misses Q ) by A6; :: thesis: verum