let T be non empty TopSpace; :: thesis: 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 )
let B be prebasis of T; :: thesis: ( 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 )
set x = the carrier of T;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then reconsider x = the carrier of T as Element of (InclPoset the topology of T) by YELLOW_1:1;
( x is compact iff x << x ) by WAYBEL_3:def 2;
hence ( 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 ) by WAYBEL_3:37, WAYBEL_7:31; :: thesis: verum