let T be non empty discrete TopSpace; :: thesis: T is regular
let p be Point of T; :: according to COMPTS_1:def 2 :: thesis: for b1 being Element of bool the carrier of T holds
( b1 = {} or 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: ( P = {} or 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
P <> {} and
P is closed and
A1: 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 )
take W = {p}; :: thesis: ex b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & P c= b1 & W misses b1 )
take V = P; :: thesis: ( W is open & V is open & p in W & P c= V & W misses V )
thus ( W is open & V is open ) by TDLAT_3:15; :: thesis: ( p in W & P c= V & W misses V )
A2: not p in P by A1, XBOOLE_0:def 5;
W /\ V c= {}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in W /\ V or a in {} )
assume A3: a in W /\ V ; :: thesis: a in {}
assume not a in {} ; :: thesis: contradiction
( a in W & a in V ) by A3, XBOOLE_0:def 4;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum
end;
hence ( p in W & P c= V & W /\ V = {} ) by TARSKI:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum