let X be non empty TopSpace; :: thesis: ( X is compact implies X is locally-compact )
set Y = [#] X;
assume A1: X is compact ; :: thesis: X is locally-compact
let x be Point of X; :: according to COMPACT1:def 6 :: thesis: ex U being a_neighborhood of x st U is compact
Int ([#] X) = [#] X by TOPS_1:23;
then [#] X is a_neighborhood of x by CONNSP_2:def 1;
hence ex U being a_neighborhood of x st U is compact by A1; :: thesis: verum