:: deftheorem defines compact COMPACT1:def 1 :
for X being TopSpace
for P being Subset-Family of X holds
( P is compact iff for U being Subset of X st U in P holds
U is compact );