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 ) )
assume A10: 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
A11: ( 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 A11, TOPS_1:23;
then consider Q being Subset of T such that
A12: Q is closed and
A13: Q c= P ` and
A14: p in Int Q by A10;
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 A12; :: thesis: ( p in W & P c= V & W misses V )
thus p in W by A14; :: thesis: ( P c= V & W misses V )
(P `) ` c= V by A13, 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