let T be non empty TopStruct ; :: thesis: ( 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 ) )
thus ( T is compact implies 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 ) ) :: thesis: ( ( 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 ) ) implies T is compact )

proof

assume A1: T is compact ; :: thesis: 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 )
let F be Subset-Family of T; :: thesis: ( F is open & [#] T c= union F implies ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) )
assume that
A2: F is open and
A3: [#] T c= union F ; :: thesis: ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite )
the carrier of T c= union F by A3;
then F is Cover of T by TOPMETR:1;
then consider G being Subset-Family of T such that
A4: G c= F and
A5: G is Cover of T and
A6: G is finite by A1, A2, COMPTS_1:def 3;
take G ; :: thesis: ( G c= F & [#] T c= union G & G is finite )
the carrier of T c= union G by A5, TOPMETR:1;
hence ( G c= F & [#] T c= union G & G is finite ) by A4, A6; :: thesis: verum

end;

assume A7: 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 ) ; :: thesis: T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def 3 :: thesis: ( not F is M4(the carrier of T) or not F is open or ex b₁ being Element of bool (bool the carrier of T) st
( b₁ c= F & b₁ is M4(the carrier of T) & b₁ is finite ) )
assume that
A8: F is Cover of T and
A9: F is open ; :: thesis: ex b₁ being Element of bool (bool the carrier of T) st
( b₁ c= F & b₁ is M4(the carrier of T) & b₁ is finite )
the carrier of T c= union F by A8, TOPMETR:1;
then [#] T c= union F ;
then consider G being Subset-Family of T such that
A10: G c= F and
A11: [#] T c= union G and
A12: G is finite by A7, A9;
take G ; :: thesis: ( G c= F & G is M4(the carrier of T) & G is finite )
the carrier of T c= union G by A11;
hence ( G c= F & G is M4(the carrier of T) & G is finite ) by A10, A12, TOPMETR:1; :: thesis: verum