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

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

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

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

A2: P is closed and

A3: 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} )

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

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

let p be Point of T; :: according to PRE_TOPC:def 11 :: thesis: for b

( not b

( b

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

( b

assume that

A2: P is closed and

A3: p in P ` ; :: thesis: ex b

( b

per cases
( P = {} or P <> {} )
;

end;

suppose A4:
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} )

( b

take G1 = [#] T; :: thesis: ex b_{1} being Element of bool the carrier of T st

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

take G2 = {} T; :: thesis: ( G1 is open & G2 is open & p in G1 & P c= G2 & G1 misses G2 )

thus ( G1 is open & G2 is open ) ; :: thesis: ( p in G1 & P c= G2 & G1 misses G2 )

thus p in G1 ; :: thesis: ( P c= G2 & G1 misses G2 )

thus ( P c= G2 & G1 misses G2 ) by A4; :: thesis: verum

end;( G1 is open & b

take G2 = {} T; :: thesis: ( G1 is open & G2 is open & p in G1 & P c= G2 & G1 misses G2 )

thus ( G1 is open & G2 is open ) ; :: thesis: ( p in G1 & P c= G2 & G1 misses G2 )

thus p in G1 ; :: thesis: ( P c= G2 & G1 misses G2 )

thus ( P c= G2 & G1 misses G2 ) by A4; :: thesis: verum

suppose
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} )

( b

hence
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} )
by A1, A2, A3; :: thesis: verum

end;( b