:: deftheorem Def3 defines liminally-compact COMPACT1:def 3 :
for X being non empty TopSpace holds
( X is liminally-compact iff for x being Point of X ex B being basis of x st B is compact );