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<sub>1</sub> being Element of bool the carrier of T holds
( not b<sub>1</sub> is closed or not p in b<sub>1</sub> ` or ex b₂, b₃ being Element of bool the carrier of T st
( b₂ is open & b₃ is open & p in b₂ & b₁ c= b₃ & b₂ misses b₃ ) )
let P be Subset of T; :: thesis: ( not P is closed or not p in P ` or ex b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of T st
( b<sub>1</sub> is open & b<sub>2</sub> is open & p in b<sub>1</sub> & P c= b<sub>2</sub> & b<sub>1</sub> misses b<sub>2</sub> ) )
assume that
A2: P is closed and
A3: p in P ` ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & p in b₁ & P c= b₂ & b₁ misses b₂ )