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:
reconsider C = COMPLEMENT F as Subset-Family of T ;
assume A4: meet F = {} ; :: thesis: contradiction
F <> {} by ;
then union () = (meet F) ` by TOPS_2:7
.= [#] T by A4 ;
then A5: COMPLEMENT F is Cover of T by SETFAM_1:def 11;
COMPLEMENT F is open by ;
then consider G9 being Subset-Family of T such that
A6: G9 c= C and
A7: G9 is Cover of T and
A8: G9 is finite by A1, A5;
set F9 = COMPLEMENT G9;
A9: COMPLEMENT G9 is finite by ;
A10: COMPLEMENT G9 c= F
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in COMPLEMENT G9 or X in F )
assume A11: X in COMPLEMENT G9 ; :: thesis: X in F
then reconsider X1 = X as Subset of T ;
X1 ` in G9 by ;
then (X1 `) ` in F by ;
hence X in F ; :: thesis: verum
end;
G9 <> {} by ;
then A12: COMPLEMENT G9 <> {} by TOPS_2:5;
meet () = (union G9) ` by
.= ([#] T) \ ([#] T) by
.= {} by XBOOLE_1:37 ;
hence contradiction by A2, A10, A9, A12, FINSET_1:def 3; :: thesis: verum
end;
assume A13: 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 1 :: 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
A14: F is Cover of T and
A15: 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 ;
A16: G is closed by ;
F <> {} by ;
then A17: G <> {} by TOPS_2:5;
meet G = () ` by
.= ([#] T) \ ([#] T) by
.= {} by XBOOLE_1:37 ;
then not G is centered by ;
then consider G9 being set such that
A18: G9 <> {} and
A19: G9 c= G and
A20: G9 is finite and
A21: meet G9 = {} by ;
reconsider G9 = G9 as Subset-Family of T by ;
take F9 = COMPLEMENT G9; :: thesis: ( F9 c= F & F9 is Cover of T & F9 is finite )
thus F9 c= F :: thesis: ( F9 is Cover of T & F9 is finite )
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in F9 or A in F )
assume A22: A in F9 ; :: thesis: A in F
then reconsider A1 = A as Subset of T ;
A1 ` in G9 by ;
then (A1 `) ` in F by ;
hence A in F ; :: thesis: verum
end;
union F9 = (meet G9) ` by
.= [#] T by A21 ;
hence F9 is Cover of T by SETFAM_1:def 11; :: thesis: F9 is finite
thus F9 is finite by ; :: thesis: verum
end;