let TS be non empty TopSpace; :: thesis: ( TS is Hausdorff & TS is compact implies TS is regular )
assume that
A1: TS is Hausdorff and
A2: TS is compact ; :: thesis: TS is regular
let p be Point of TS; :: according to COMPTS_1:def 2 :: thesis: for P being Subset of TS st P <> {} & P is closed & p in P ` holds
ex W, V being Subset of TS st
( W is open & V is open & p in W & P c= V & W misses V )
let F be Subset of TS; :: thesis: ( F <> {} & F is closed & p in F ` implies ex W, V being Subset of TS st
( W is open & V is open & p in W & F c= V & W misses V ) )
assume that
A3: F <> {} and
A4: F is closed and
A5: p in F ` ; :: thesis: ex W, V being Subset of TS st
( W is open & V is open & p in W & F c= V & W misses V )
thus ex W, V being Subset of TS st
( W is open & V is open & p in W & F c= V & W misses V ) by A1, A2, A3, A4, A5, Th15, Th17; :: thesis: verum