for T being non empty TopSpace
for B being prebasis of T holds
( T is compact iff for F being Subset of B st [#] T c= union F holds
ex G being finite Subset of F st [#] T c= union G )