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 )

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 <> {}

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 A9:
for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds
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;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

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

hence
T is compact
by Th4; :: thesis: verum
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;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