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 )
F is Cover of T by A3, TOPMETR:1;
then consider G being Subset-Family of T such that
A4: ( G c= F & G is Cover of T & G is finite ) by A1, A2;
take G ; :: thesis: ( G c= F & [#] T c= union G & G is finite )
thus ( G c= F & [#] T c= union G & G is finite ) by A4, TOPMETR:1; :: thesis: verum
end;
assume A5: 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 1 :: thesis: ( not F is M5( the carrier of T) or not F is open or ex b1 being Element of bool (bool the carrier of T) st
( b1 c= F & b1 is M5( the carrier of T) & b1 is finite ) )
assume that
A6: F is Cover of T and
A7: F is open ; :: thesis: ex b1 being Element of bool (bool the carrier of T) st
( b1 c= F & b1 is M5( the carrier of T) & b1 is finite )
[#] T c= union F by A6, TOPMETR:1;
then consider G being Subset-Family of T such that
A8: ( G c= F & [#] T c= union G & G is finite ) by A5, A7;
take G ; :: thesis: ( G c= F & G is M5( the carrier of T) & G is finite )
thus ( G c= F & G is M5( the carrier of T) & G is finite ) by A8, TOPMETR:1; :: thesis: verum