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:12, COMPTS_1:13; :: thesis: T is locally-compact
A3: [#] T is compact by A1;
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 that
A4: x in X and
A5: X is open ; :: thesis: ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
consider Y being open Subset of T such that
A6: x in Y and
A7: Cl Y c= X by A2, A4, A5, URYSOHN1:21;
take Z = Cl Y; :: thesis: ( x in Int Z & Z c= X & Z is compact )
Y c= Int Z by PRE_TOPC:18, TOPS_1:24;
hence ( x in Int Z & Z c= X & Z is compact ) by A3, A6, A7, COMPTS_1:9; :: thesis: verum