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

proof

assume A1: T is compact ; :: thesis: for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} )
let F be Subset-Family of T; :: thesis: ( F <> {} & F is closed & meet F = {} implies ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) )
assume that
A2: F <> {} and
A3: F is closed and
A4: meet F = {} ; :: thesis: ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} )
not F is centered by A1, A3, A4, Th13;
then consider G being set such that
A5: ( G <> {} & G c= F & G is finite & meet G = {} ) by A2, FINSET_1:def 3;
reconsider G = G as Subset-Family of T by A5, XBOOLE_1:1;
take X = G; :: thesis: ( X <> {} & X c= F & X is finite & meet X = {} )
thus ( X <> {} & X c= F & X is finite & meet X = {} ) by A5; :: thesis: verum

end;

assume A6: for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) ; :: thesis: T is compact
for F being Subset-Family of T st F is centered & F is closed holds
meet F <> {}

proof

let F be Subset-Family of T; :: thesis: ( F is centered & F is closed implies meet F <> {} )
assume that
A7: F is centered and
A8: F is closed ; :: thesis: meet F <> {}
assume A9: meet F = {} ; :: thesis: contradiction
F <> {} by A7, FINSET_1:def 3;
then ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) by A6, A8, A9;
hence contradiction by A7, FINSET_1:def 3; :: thesis: verum

end;

hence T is compact by Th13; :: thesis: verum