for T being non empty TopStruct holds
( T is compact iff for F being Subset-Family of T st F is open & [#] T c= union F holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) )