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₂ )

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

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

take G1 = [#] T; :: thesis: ex b₁ being Element of bool the carrier of T st
( G1 is open & b₁ is open & p in G1 & P c= b₁ & G1 misses 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

end;

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

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

end;

end;