let T be non empty TopSpace; :: thesis: ( T is compact & T is T_2 implies ( T is regular & T is normal & T is locally-compact ) )
assume A1: ( T is compact & T is T_2 ) ; :: thesis: ( T is regular & T is normal & T is locally-compact )
hence A2: ( T is regular & T is normal ) by COMPTS_1:21, COMPTS_1:22; :: thesis: T is locally-compact
A3: ( [#] T is compact & [#] T = the carrier of T ) by A1, COMPTS_1:10;
let x be Point of T; :: according to WAYBEL_3:def 9 :: thesis: for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
let X be Subset of T; :: thesis: ( x in X & X is open implies ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact ) )
assume ( x in X & X is open ) ; :: thesis: ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
then consider Y being open Subset of T such that
A4: ( x in Y & Cl Y c= X ) by A2, URYSOHN1:29;
take Z = Cl Y; :: thesis: ( x in Int Z & Z c= X & Z is compact )
( Y c= Int Z & Z is closed ) by PRE_TOPC:48, TOPS_1:56;
hence ( x in Int Z & Z c= X & Z is compact ) by A3, A4, COMPTS_1:18; :: thesis: verum