let T be non empty TopSpace; :: thesis:
thus ( T is regular implies for A being open Subset of T
for p being Point of T st p in A holds
ex B being open Subset of T st
( p in B & Cl B c= A ) ) :: thesis:

assume A1: T is regular ; :: thesis:
thus for A being open Subset of T
for p being Point of T st p in A holds
ex B being open Subset of T st
( p in B & Cl B c= A ) :: thesis:

reconsider P = A ` as Subset of T ;

end;

end;

hence ex B being open Subset of T st
( p in B & Cl B c= A ) ; :: thesis:

end;

assume A11: for A being open Subset of T
for p being Point of T st p in A holds
ex B being open Subset of T st
( p in B & Cl B c= A ) ; :: thesis:
for p being Point of T
for P being Subset of T st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V )

let p be Point of T; :: thesis:
let P be Subset of T; :: thesis:
assume that
P <> {} and
A12: ( P is closed & p in P ` ) ; :: thesis:
thus ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) :: thesis:

consider A being Subset of T such that
A13: A = P ` ;
consider B being open Subset of T such that
A14: ( p in B & Cl B c= A ) by A11, A12, A13;
consider C being Subset of T such that
A15: C = ([#] T) \ (Cl B) ;
reconsider B = B, C = C as Subset of T ;
Cl B misses C by A15, XBOOLE_1:79;
then A16: B misses C by PRE_TOPC:18, XBOOLE_1:63;
take B ; :: thesis:
take C ; :: thesis:
( (Cl B) ` is open & (P `) ` = P ) ;
hence ( B is open & C is open & p in B & P c= C & B misses C ) by A13, A14, A15, A16, XBOOLE_1:34; :: thesis:

end;