let T be non empty TopSpace; :: thesis: ( T is regular iff for p being Point of T

for P being Subset of T st p in Int P holds

ex Q being Subset of T st

( Q is closed & Q c= P & p in Int Q ) )

for P being Subset of T st p in Int P holds

ex Q being Subset of T st

( Q is closed & Q c= P & p in Int Q ) ; :: thesis: T is regular

let p be Point of T; :: according to COMPTS_1:def 2 :: thesis: for b_{1} being Element of bool the carrier of T holds

( b_{1} = {} or not b_{1} is closed or not p in b_{1} ` or ex b_{2}, b_{3} being Element of bool the carrier of T st

( b_{2} is open & b_{3} is open & p in b_{2} & b_{1} c= b_{3} & b_{2} misses b_{3} ) )

let P be Subset of T; :: thesis: ( P = {} or not P is closed or not p in P ` or ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & p in b_{1} & P c= b_{2} & b_{1} misses b_{2} ) )

assume that

P <> {} and

A11: ( P is closed & p in P ` ) ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & p in b_{1} & P c= b_{2} & b_{1} misses b_{2} )

p in Int (P `) by A11, TOPS_1:23;

then consider Q being Subset of T such that

A12: Q is closed and

A13: Q c= P ` and

A14: p in Int Q by A10;

reconsider W = Int Q as Subset of T ;

take W ; :: thesis: ex b_{1} being Element of bool the carrier of T st

( W is open & b_{1} is open & p in W & P c= b_{1} & W misses b_{1} )

take V = Q ` ; :: thesis: ( W is open & V is open & p in W & P c= V & W misses V )

thus W is open ; :: thesis: ( V is open & p in W & P c= V & W misses V )

thus V is open by A12; :: thesis: ( p in W & P c= V & W misses V )

thus p in W by A14; :: thesis: ( P c= V & W misses V )

(P `) ` c= V by A13, SUBSET_1:12;

hence P c= V ; :: thesis: W misses V

Q misses V by XBOOLE_1:79;

hence W misses V by TOPS_1:16, XBOOLE_1:63; :: thesis: verum

for P being Subset of T st p in Int P holds

ex Q being Subset of T st

( Q is closed & Q c= P & p in Int Q ) )

hereby :: thesis: ( ( for p being Point of T

for P being Subset of T st p in Int P holds

ex Q being Subset of T st

( Q is closed & Q c= P & p in Int Q ) ) implies T is regular )

assume A10:
for p being Point of Tfor P being Subset of T st p in Int P holds

ex Q being Subset of T st

( Q is closed & Q c= P & p in Int Q ) ) implies T is regular )

assume A1:
T is regular
; :: thesis: for p being Point of T

for P being Subset of T st p in Int P holds

ex Q being Element of bool the carrier of T st

( b_{5} is closed & b_{5} c= b_{4} & Q in Int b_{5} )

let p be Point of T; :: thesis: for P being Subset of T st p in Int P holds

ex Q being Element of bool the carrier of T st

( b_{4} is closed & b_{4} c= b_{3} & Q in Int b_{4} )

let P be Subset of T; :: thesis: ( p in Int P implies ex Q being Element of bool the carrier of T st

( b_{3} is closed & b_{3} c= b_{2} & Q in Int b_{3} ) )

assume p in Int P ; :: thesis: ex Q being Element of bool the carrier of T st

( b_{3} is closed & b_{3} c= b_{2} & Q in Int b_{3} )

then A2: p in ((Int P) `) ` ;

end;for P being Subset of T st p in Int P holds

ex Q being Element of bool the carrier of T st

( b

let p be Point of T; :: thesis: for P being Subset of T st p in Int P holds

ex Q being Element of bool the carrier of T st

( b

let P be Subset of T; :: thesis: ( p in Int P implies ex Q being Element of bool the carrier of T st

( b

assume p in Int P ; :: thesis: ex Q being Element of bool the carrier of T st

( b

then A2: p in ((Int P) `) ` ;

per cases
( P = [#] T or P <> [#] T )
;

end;

suppose A3:
P = [#] T
; :: thesis: ex Q being Element of bool the carrier of T st

( b_{3} is closed & b_{3} c= b_{2} & Q in Int b_{3} )

( b

take Q = [#] T; :: thesis: ( Q is closed & Q c= P & p in Int Q )

thus Q is closed ; :: thesis: ( Q c= P & p in Int Q )

thus Q c= P by A3; :: thesis: p in Int Q

Int Q = Q by TOPS_1:15;

hence p in Int Q ; :: thesis: verum

end;thus Q is closed ; :: thesis: ( Q c= P & p in Int Q )

thus Q c= P by A3; :: thesis: p in Int Q

Int Q = Q by TOPS_1:15;

hence p in Int Q ; :: thesis: verum

suppose
P <> [#] T
; :: thesis: ex Q being Element of bool the carrier of T st

( b_{3} is closed & b_{3} c= b_{2} & Q in Int b_{3} )

( b

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: (Int P) ` c= V and

A8: W misses V by A1, A2;

A9: Int P c= P by TOPS_1:16;

take Q = V ` ; :: thesis: ( Q is closed & Q c= P & p in Int Q )

thus Q is closed by A5; :: thesis: ( Q c= P & p in Int Q )

(Int P) ` c= Q ` by A7;

then Q c= Int P by SUBSET_1:12;

hence Q c= P by A9; :: thesis: p in Int Q

W c= Q by A8, SUBSET_1:23;

then W c= Int Q by A4, TOPS_1:24;

hence p in Int Q by A6; :: thesis: verum

end;A4: W is open and

A5: V is open and

A6: p in W and

A7: (Int P) ` c= V and

A8: W misses V by A1, A2;

A9: Int P c= P by TOPS_1:16;

take Q = V ` ; :: thesis: ( Q is closed & Q c= P & p in Int Q )

thus Q is closed by A5; :: thesis: ( Q c= P & p in Int Q )

(Int P) ` c= Q ` by A7;

then Q c= Int P by SUBSET_1:12;

hence Q c= P by A9; :: thesis: p in Int Q

W c= Q by A8, SUBSET_1:23;

then W c= Int Q by A4, TOPS_1:24;

hence p in Int Q by A6; :: thesis: verum

for P being Subset of T st p in Int P holds

ex Q being Subset of T st

( Q is closed & Q c= P & p in Int Q ) ; :: thesis: T is regular

let p be Point of T; :: according to COMPTS_1:def 2 :: thesis: for b

( b

( b

let P be Subset of T; :: thesis: ( P = {} or not P is closed or not p in P ` or ex b

( b

assume that

P <> {} and

A11: ( P is closed & p in P ` ) ; :: thesis: ex b

( b

p in Int (P `) by A11, TOPS_1:23;

then consider Q being Subset of T such that

A12: Q is closed and

A13: Q c= P ` and

A14: p in Int Q by A10;

reconsider W = Int Q as Subset of T ;

take W ; :: thesis: ex b

( W is open & b

take V = Q ` ; :: thesis: ( W is open & V is open & p in W & P c= V & W misses V )

thus W is open ; :: thesis: ( V is open & p in W & P c= V & W misses V )

thus V is open by A12; :: thesis: ( p in W & P c= V & W misses V )

thus p in W by A14; :: thesis: ( P c= V & W misses V )

(P `) ` c= V by A13, SUBSET_1:12;

hence P c= V ; :: thesis: W misses V

Q misses V by XBOOLE_1:79;

hence W misses V by TOPS_1:16, XBOOLE_1:63; :: thesis: verum