:: deftheorem defines locally-compact WAYBEL_3:def 9 :
for T being non empty TopSpace holds
( T is locally-compact iff for x being Point of T
for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact ) );