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 A5, TOPS_1:13;
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 A7, XBOOLE_1:63;
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 A9, SUBSET_1:23;
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 A10, PRE_TOPC:4;
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 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: 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 A13, A14, A15, A16, XBOOLE_1:34; :: thesis: verum

end;

end;

hence T is regular by COMPTS_1:def 2; :: thesis: verum