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

proof

assume A1: T is compact ; :: thesis: for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {}
let F be Subset-Family of T; :: thesis: ( F is centered & F is closed implies meet F <> {} )
assume that
A2: F is centered and
A3: F is closed ; :: thesis: meet F <> {}
assume A4: meet F = {} ; :: thesis: contradiction
reconsider C = COMPLEMENT F as Subset-Family of T ;
F <> {} by A2, FINSET_1:def 3;
then union (COMPLEMENT F) = (meet F) ` by TOPS_2:12
.= [#] T by A4 ;
then A5: COMPLEMENT F is Cover of T by SETFAM_1:def 12;
COMPLEMENT F is open by A3, TOPS_2:16;
then consider G' being Subset-Family of T such that
A6: G' c= C and
A7: G' is Cover of T and
A8: G' is finite by A1, A5, Def3;
set F' = COMPLEMENT G';
A9: 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 A10: X in COMPLEMENT G' ; :: thesis: X in F
then reconsider X1 = X as Subset of T ;
X1 ` in G' by A10, SETFAM_1:def 8;
then (X1 ` ) ` in F by A6, SETFAM_1:def 8;
hence X in F ; :: thesis: verum

end;

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

end;

assume A14: for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {} ; :: thesis: T is compact
thus T is compact :: thesis: verum

proof

let F be Subset-Family of T; :: according to COMPTS_1:def 3 :: thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite ) )
assume that
A15: F is Cover of T and
A16: F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of T & G is finite )
reconsider G = COMPLEMENT F as Subset-Family of T ;
A17: G is closed by A16, TOPS_2:17;
A18: F <> {} by A15, TOPS_2:5;
A19: meet G = (union F) ` by A15, TOPS_2:5, TOPS_2:11
.= ([#] T) \ ([#] T) by A15, SETFAM_1:60
.= {} by XBOOLE_1:37 ;
A20: G <> {} by A18, TOPS_2:10;
not G is centered by A14, A17, A19;
then consider G' being set such that
A21: G' <> {} and
A22: G' c= G and
A23: G' is finite and
A24: meet G' = {} by A20, FINSET_1:def 3;
reconsider G' = G' as Subset-Family of T by A22, 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 A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in F' or A in F )
assume A25: A in F' ; :: thesis: A in F
then reconsider A1 = A as Subset of T ;
A1 ` in G' by A25, SETFAM_1:def 8;
then (A1 ` ) ` in F by A22, SETFAM_1:def 8;
hence A in F ; :: thesis: verum

end;

union F' = (meet G') ` by A21, TOPS_2:12
.= [#] T by A24 ;
hence F' is Cover of T by SETFAM_1:def 12; :: thesis: F' is finite
thus F' is finite by A23, TOPS_2:13; :: thesis: verum

end;