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