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

( 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