let T be non empty TopSpace; :: thesis: ( T is regular iff for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) )

hereby :: thesis: ( ( for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) ) implies T is regular )

assume A1: T is regular ; :: thesis: for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Element of bool the carrier of T st
( b₅ is closed & b₅ c= b₄ & Q in Int b₅ )
let p be Point of T; :: thesis: for P being Subset of T st p in Int P holds
ex Q being Element of bool the carrier of T st
( b₄ is closed & b₄ c= b₃ & Q in Int b₄ )
let P be Subset of T; :: thesis: ( p in Int P implies ex Q being Element of bool the carrier of T st
( b₃ is closed & b₃ c= b₂ & Q in Int b₃ ) )
assume p in Int P ; :: thesis: ex Q being Element of bool the carrier of T st
( b₃ is closed & b₃ c= b₂ & Q in Int b₃ )
then A2: p in ((Int P) `) ` ;

per cases ( P = [#] T or P <> [#] T ) ;

suppose A3: P = [#] T ; :: thesis: ex Q being Element of bool the carrier of T st
( b₃ is closed & b₃ c= b₂ & Q in Int b₃ )

take Q = [#] T; :: thesis: ( Q is closed & Q c= P & p in Int Q )
thus Q is closed ; :: thesis: ( Q c= P & p in Int Q )
thus Q c= P by A3; :: thesis: p in Int Q
Int Q = Q by TOPS_1:15;
hence p in Int Q ; :: thesis: verum

end;

suppose A4: P <> [#] T ; :: thesis: ex Q being Element of bool the carrier of T st
( b₃ is closed & b₃ c= b₂ & Q in Int b₃ )

now

assume (Int P) ` = {} ; :: thesis: contradiction
then ((Int P) `) ` = [#] T ;
then [#] T c= P by TOPS_1:16;
hence contradiction by A4, XBOOLE_0:def 10; :: thesis: verum

end;

then consider W, V being Subset of T such that
A5: W is open and
A6: V is open and
A7: p in W and
A8: (Int P) ` c= V and
A9: W misses V by A1, A2, COMPTS_1:def 2;
A10: Int P c= P by TOPS_1:16;
take Q = V ` ; :: thesis: ( Q is closed & Q c= P & p in Int Q )
thus Q is closed by A6; :: thesis: ( Q c= P & p in Int Q )
(Int P) ` c= Q ` by A8;
then Q c= Int P by SUBSET_1:12;
hence Q c= P by A10, XBOOLE_1:1; :: thesis: p in Int Q
W c= Q by A9, SUBSET_1:23;
then W c= Int Q by A5, TOPS_1:24;
hence p in Int Q by A7; :: thesis: verum

end;

end;

end;

assume A11: for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) ; :: 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
A12: ( P is closed & p in P ` ) ; :: thesis: ex b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of T st
( b<sub>1</sub> is open & b<sub>2</sub> is open & p in b<sub>1</sub> & P c= b<sub>2</sub> & b<sub>1</sub> misses b<sub>2</sub> )
p in Int (P `) by A12, TOPS_1:23;
then consider Q being Subset of T such that
A13: Q is closed and
A14: Q c= P ` and
A15: p in Int Q by A11;
reconsider W = Int Q as Subset of T ;
take W ; :: thesis: ex b<sub>1</sub> being Element of bool the carrier of T st
( W is open & b<sub>1</sub> is open & p in W & P c= b<sub>1</sub> & W misses b<sub>1</sub> )
take V = Q ` ; :: thesis: ( W is open & V is open & p in W & P c= V & W misses V )
thus W is open ; :: thesis: ( V is open & p in W & P c= V & W misses V )
thus V is open by A13; :: thesis: ( p in W & P c= V & W misses V )
thus p in W by A15; :: thesis: ( P c= V & W misses V )
(P `) ` c= V by A14, SUBSET_1:12;
hence P c= V ; :: thesis: W misses V
Q misses V by XBOOLE_1:79;
hence W misses V by TOPS_1:16, XBOOLE_1:63; :: thesis: verum