let X be non empty TopSpace; :: thesis: ( X is discrete implies X is locally-compact )

assume A1: X is discrete ; :: 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

set Y = {x};

{x} is open by A1, TDLAT_3:15;

then Int {x} = {x} by TOPS_1:23;

then x in Int {x} by TARSKI:def 1;

then reconsider Y = {x} as a_neighborhood of x by CONNSP_2:def 1;

Y is compact ;

hence ex U being a_neighborhood of x st U is compact ; :: thesis: verum

assume A1: X is discrete ; :: 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

set Y = {x};

{x} is open by A1, TDLAT_3:15;

then Int {x} = {x} by TOPS_1:23;

then x in Int {x} by TARSKI:def 1;

then reconsider Y = {x} as a_neighborhood of x by CONNSP_2:def 1;

Y is compact ;

hence ex U being a_neighborhood of x st U is compact ; :: thesis: verum