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

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