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 )

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 b_{1} being Element of bool (bool the carrier of T) st

( b_{1} c= F & b_{1} is M5( the carrier of T) & b_{1} is finite ) )

assume that

A6: F is Cover of T and

A7: F is open ; :: thesis: ex b_{1} being Element of bool (bool the carrier of T) st

( b_{1} c= F & b_{1} is M5( the carrier of T) & b_{1} 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

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 A5:
for F being Subset-Family of T st F is open & [#] T c= union F holds
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;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

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 b

( b

assume that

A6: F is Cover of T and

A7: F is open ; :: thesis: ex b

( b

[#] 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