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
( b5 is closed & b5 c= b4 & Q in Int b5 )

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
( b4 is closed & b4 c= b3 & Q in Int b4 )

let P be Subset of T; :: thesis: ( p in Int P implies ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 ) )

assume p in Int P ; :: thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )

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
( b3 is closed & b3 c= b2 & Q in Int b3 )

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 P <> [#] T ; :: thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )

consider W, V being Subset of T such that
A4: W is open and
A5: V is open and
A6: p in W and
A7: (Int P) ` c= V and
A8: W misses V by A1, A2;
A9: 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 A5; :: thesis: ( Q c= P & p in Int Q )
(Int P) ` c= Q ` by A7;
then Q c= Int P by SUBSET_1:12;
hence Q c= P by A9; :: thesis: p in Int Q
W c= Q by ;
then W c= Int Q by ;
hence p in Int Q by A6; :: thesis: verum
end;
end;
end;
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 b1 being Element of bool the carrier of T holds
( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )

let P be Subset of T; :: thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )

assume that
P <> {} and
A11: ( P is closed & p in P ` ) ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )

p in Int (P `) by ;
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 b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & P c= b1 & W misses b1 )

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 ;
hence P c= V ; :: thesis: W misses V
Q misses V by XBOOLE_1:79;
hence W misses V by ; :: thesis: verum