:: deftheorem Def2 defines relatively-compact COMPACT1:def 2 :
for X being TopSpace
for U being Subset of X holds
( U is relatively-compact iff Cl U is compact );