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 )

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 )

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 A11:
for A being open Subset of T
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

end;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

end;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 ;

( p in B & Cl B c= A ) ; :: thesis: verum

end;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 ) ) )end;

hence
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 = {} )
;

end;

case
P <> {}
; :: thesis: ex W being Subset of T ex B being open Subset of T st

( p in B & Cl B c= A )

( 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;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

( p in B & Cl B c= A ) ; :: thesis: verum

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

hence
T is regular
by COMPTS_1:def 2; :: thesis: verum
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

end;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;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