let T be non empty TopSpace; :: thesis: ( T is regular iff 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 ) )

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: ( ( 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 ) ) implies T is regular )
proof
assume A1: T is regular ; :: thesis: 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 )

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: verum
proof
let A be open Subset of T; :: thesis: 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 )

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

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

then A3: p in (A `) ` ;
thus ex B being open Subset of T st
( p in B & Cl B c= A ) :: thesis: verum
proof
reconsider P = A ` as Subset of T ;
now :: thesis: ( ( P <> {} & ex W being Subset of T ex B being open Subset of T st
( p in B & Cl B c= A ) ) or ( P = {} & ex A, B being open Subset of T st
( p in B & Cl B c= A ) ) )
per cases ( P <> {} or P = {} ) ;
case P <> {} ; :: thesis: ex W being Subset of T ex B being open Subset of T st
( p in B & Cl B c= A )

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: P c= V and
A8: W misses V by A1, A3;
W /\ V = {} by A8;
then V /\ (Cl W) c= Cl ({} T) by ;
then V /\ (Cl W) c= {} by PRE_TOPC:22;
then V /\ (Cl W) = {} ;
then V misses Cl W ;
then A9: P misses Cl W by ;
take W = W; :: thesis: ex B being open Subset of T st
( p in B & Cl B c= A )

(A `) ` = A ;
then Cl W c= A by ;
hence ex B being open Subset of T st
( p in B & Cl B c= A ) by A4, A6; :: thesis: verum
end;
case A10: P = {} ; :: thesis: ex A, B being open Subset of T st
( p in B & Cl B c= A )

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

A = [#] T by ;
then Cl A c= A ;
hence ex B being open Subset of T st
( p in B & Cl B c= A ) by A2; :: thesis: verum
end;
end;
end;
hence ex B being open Subset of T st
( p in B & Cl B c= A ) ; :: thesis: verum
end;
end;
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: T is regular
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 )
proof
let p be Point of T; :: thesis: 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 Subset of T; :: thesis: ( P <> {} & P is closed & p in P ` implies ex W, V being Subset of T st
( W is open & V is open & p in W & P c= V & W misses V ) )

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

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: verum
proof
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 ;
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 ;
then A16: B misses C by ;
take B ; :: thesis: ex V being Subset of T st
( B is open & V is open & p in B & P c= V & B misses V )

take C ; :: thesis: ( B is open & C is open & p in B & P c= C & B misses C )
( (Cl B) ` is open & (P `) ` = P ) ;
hence ( B is open & C is open & p in B & P c= C & B misses C ) by ; :: thesis: verum
end;
end;
hence T is regular by COMPTS_1:def 2; :: thesis: verum