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, Th4;
then consider G being set such that
A5: G <> {} and
A6: G c= F and
A7: G is finite and
A8: meet G = {} by A2, FINSET_1:def 3;
reconsider G = G as Subset-Family of T by A6, XBOOLE_1:1;
take G ; :: thesis: ( G <> {} & G c= F & G is finite & meet G = {} )
thus ( G <> {} & G c= F & G is finite & meet G = {} ) by A5, A6, A7, A8; :: thesis: verum

end;

assume A9: 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
A10: F is centered and
A11: F is closed ; :: thesis: meet F <> {}
assume A12: meet F = {} ; :: thesis: contradiction
F <> {} by A10, FINSET_1:def 3;
then ex G being Subset-Family of T st
( G <> {} & G c= F & G is finite & meet G = {} ) by A9, A11, A12;
hence contradiction by A10, FINSET_1:def 3; :: thesis: verum

end;

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