:: deftheorem Def4 defines compact COMPTS_1:def 4 :
for T being TopStruct
for P being Subset of T holds
( P is compact iff for F being Subset-Family of T st F is Cover of P & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of P & G is finite ) );