let T be non empty TopSpace; :: thesis:
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:

assume A1: T is compact ; :: thesis:
let F be Subset-Family of T; :: thesis:
assume that
A2: F <> {} and
A3: F is closed and
A4: meet F = {} ; :: thesis:
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:
thus ( G <> {} & G c= F & G is finite & meet G = {} ) by A5, A6, A7, A8; :: thesis:

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:
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:
assume that
A10: F is centered and
A11: F is closed ; :: thesis:
assume A12: meet F = {} ; :: thesis:
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:

end;

hence T is compact by Th4; :: thesis: