:: deftheorem Def6 defines locally-compact COMPACT1:def 6 :
for X being non empty TopSpace holds
( X is locally-compact iff for x being Point of X ex U being a_neighborhood of x st U is compact );