let T be non empty TopSpace; :: thesis: ( T is countably_compact iff for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} )
thus ( T is countably_compact implies for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} ) :: thesis: ( ( for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} ) implies T is countably_compact )

proof

assume A1: T is countably_compact ; :: thesis: for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {}
let F be Subset-Family of T; :: thesis: ( F is centered & F is closed & F is countable implies meet F <> {} )
assume that
A2: ( F is centered & F is closed ) and
A3: F is countable ; :: thesis: meet F <> {}
assume A4: meet F = {} ; :: thesis: contradiction
F <> {} by A2, FINSET_1:def 3;
then union (COMPLEMENT F) = (meet F) ` by TOPS_2:12
.= [#] T by A4 ;
then ( COMPLEMENT F is Cover of T & COMPLEMENT F is open & COMPLEMENT F is countable ) by A2, A3, SETFAM_1:60, TOPGEN_4:1, TOPS_2:16;
then consider G' being Subset-Family of T such that
A5: ( G' c= COMPLEMENT F & G' is Cover of T ) and
A6: G' is finite by A1, Def9;
A7: COMPLEMENT G' c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in COMPLEMENT G' or x in F )
assume A8: x in COMPLEMENT G' ; :: thesis: x in F
reconsider x' = x as Subset of T by A8;
x' ` in G' by A8, SETFAM_1:def 8;
then (x' ` ) ` in F by A5, SETFAM_1:def 8;
hence x in F ; :: thesis: verum

end;

A9: G' <> {} by A5, TOPS_2:5;
A10: meet (COMPLEMENT G') = (union G') ` by A5, TOPS_2:5, TOPS_2:11
.= ([#] T) \ ([#] T) by A5, SETFAM_1:60
.= {} by XBOOLE_1:37 ;
( COMPLEMENT G' <> {} & COMPLEMENT G' is finite ) by A6, A9, TOPS_2:10, TOPS_2:13;
hence contradiction by A2, A7, A10, FINSET_1:def 3; :: thesis: verum

end;

assume A11: for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {} ; :: thesis: T is countably_compact
let F be Subset-Family of T; :: according to COMPL_SP:def 9 :: thesis: ( F is Cover of T & F is open & F is countable implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume that
A12: ( F is Cover of T & F is open ) and
A13: F is countable ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
A14: ( COMPLEMENT F is countable & COMPLEMENT F is closed & F <> {} ) by A12, A13, TOPGEN_4:1, TOPS_2:5, TOPS_2:17;
then meet (COMPLEMENT F) = (union F) ` by TOPS_2:11
.= ([#] T) \ ([#] T) by A12, SETFAM_1:60
.= {} by XBOOLE_1:37 ;
then ( COMPLEMENT F <> {} & not COMPLEMENT F is centered ) by A11, A14, TOPS_2:10;
then consider G' being set such that
A15: ( G' <> {} & G' c= COMPLEMENT F ) and
A16: ( G' is finite & meet G' = {} ) by FINSET_1:def 3;
reconsider G' = G' as Subset-Family of T by A15, XBOOLE_1:1;
take F' = COMPLEMENT G'; :: thesis: ( F' c= F & F' is Cover of T & F' is finite )
thus F' c= F :: thesis: ( F' is Cover of T & F' is finite )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F' or x in F )
assume A17: x in F' ; :: thesis: x in F
reconsider x' = x as Subset of T by A17;
x' ` in G' by A17, SETFAM_1:def 8;
then (x' ` ) ` in F by A15, SETFAM_1:def 8;
hence x in F ; :: thesis: verum

end;

union F' = (meet G') ` by A15, TOPS_2:12
.= [#] T by A16 ;
hence ( F' is Cover of T & F' is finite ) by A16, SETFAM_1:60, TOPS_2:13; :: thesis: verum