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

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 )

then consider W, V being Subset of T such that
A4: ( W is open & V is open & p in W & P c= V & W misses V ) by A1, A3, COMPTS_1:def 5;
take W = W; :: thesis: ex B being open Subset of T st
( p in B & Cl B c= A )
Cl W c= A

proof

W /\ V = {} by A4, XBOOLE_0:def 7;
then V /\ (Cl W) c= Cl ({} T) by A4, TOPS_1:40;
then V /\ (Cl W) c= {} by PRE_TOPC:52;
then V /\ (Cl W) = {} ;
then V misses Cl W by XBOOLE_0:def 7;
then A5: P misses Cl W by A4, XBOOLE_1:63;
(A ` ) ` = A ;
hence Cl W c= A by A5, SUBSET_1:43; :: thesis: verum

end;

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

end;

case P = {} ; :: thesis: ex A, B being open Subset of T st
( p in B & Cl B c= A )

then A6: A = [#] T by PRE_TOPC:23;
take A = A; :: thesis: ex B being open Subset of T st
( p in B & Cl B c= A )
Cl A c= A by A6;
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 A7: 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
thus T is regular :: thesis: verum

proof

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 A8: ( P <> {} & 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
A9: A = P ` ;
consider B being open Subset of T such that
A10: ( p in B & Cl B c= A ) by A7, A8, A9;
consider C being Subset of T such that
A11: C = ([#] T) \ (Cl B) ;
reconsider B = B, C = C as Subset of T ;
A12: (Cl B) ` is open ;
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 )
( p in B & P c= C & B misses C )

proof

thus p in B by A10; :: thesis: ( P c= C & B misses C )
A13: (P ` ) ` = P ;
( B c= Cl B & Cl B misses C ) by A11, PRE_TOPC:48, XBOOLE_1:79;
hence ( P c= C & B misses C ) by A9, A10, A11, A13, XBOOLE_1:34, XBOOLE_1:63; :: thesis: verum

end;

hence ( B is open & C is open & p in B & P c= C & B misses C ) by A11, A12; :: thesis: verum

end;

end;

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

end;