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