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 b1 being Element of bool the carrier of T holds
( not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )

let P be Subset of T; :: thesis: ( not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )

assume that
A2: P is closed and
A3: p in P ` ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )

per cases ( P = {} or P <> {} ) ;
suppose A4: P = {} ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )

take G1 = [#] T; :: thesis: ex b1 being Element of bool the carrier of T st
( G1 is open & b1 is open & p in G1 & P c= b1 & G1 misses b1 )

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 b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )

hence ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) by A1, A2, A3; :: thesis: verum
end;
end;