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 )

meet F <> {} ; :: thesis: T is compact

thus T is compact :: thesis: verum

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

reconsider C = COMPLEMENT F as Subset-Family of T ;

assume A4: meet F = {} ; :: thesis: contradiction

F <> {} by A2, FINSET_1:def 3;

then union (COMPLEMENT F) = (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 A3, TOPS_2:9;

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 A8, TOPS_2:8;

A10: COMPLEMENT G9 c= F

then A12: COMPLEMENT G9 <> {} by TOPS_2:5;

meet (COMPLEMENT G9) = (union G9) ` by A7, TOPS_2:3, TOPS_2:6

.= ([#] T) \ ([#] T) by A7, SETFAM_1:45

.= {} by XBOOLE_1:37 ;

hence contradiction by A2, A10, A9, A12, FINSET_1:def 3; :: thesis: verum

end;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: meet F <> {}

reconsider C = COMPLEMENT F as Subset-Family of T ;

assume A4: meet F = {} ; :: thesis: contradiction

F <> {} by A2, FINSET_1:def 3;

then union (COMPLEMENT F) = (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 A3, TOPS_2:9;

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 A8, TOPS_2:8;

A10: COMPLEMENT G9 c= F

proof

G9 <> {}
by A7, TOPS_2:3;
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 A11, SETFAM_1:def 7;

then (X1 `) ` in F by A6, SETFAM_1:def 7;

hence X in F ; :: thesis: verum

end;assume A11: X in COMPLEMENT G9 ; :: thesis: X in F

then reconsider X1 = X as Subset of T ;

X1 ` in G9 by A11, SETFAM_1:def 7;

then (X1 `) ` in F by A6, SETFAM_1:def 7;

hence X in F ; :: thesis: verum

then A12: COMPLEMENT G9 <> {} by TOPS_2:5;

meet (COMPLEMENT G9) = (union G9) ` by A7, TOPS_2:3, TOPS_2:6

.= ([#] T) \ ([#] T) by A7, SETFAM_1:45

.= {} by XBOOLE_1:37 ;

hence contradiction by A2, A10, A9, A12, FINSET_1:def 3; :: thesis: verum

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 A15, TOPS_2:10;

F <> {} by A14, TOPS_2:3;

then A17: G <> {} by TOPS_2:5;

meet G = (union F) ` by A14, TOPS_2:3, TOPS_2:6

.= ([#] T) \ ([#] T) by A14, SETFAM_1:45

.= {} by XBOOLE_1:37 ;

then not G is centered by A13, A16;

then consider G9 being set such that

A18: G9 <> {} and

A19: G9 c= G and

A20: G9 is finite and

A21: meet G9 = {} by A17, FINSET_1:def 3;

reconsider G9 = G9 as Subset-Family of T by A19, XBOOLE_1:1;

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 )

.= [#] T by A21 ;

hence F9 is Cover of T by SETFAM_1:def 11; :: thesis: F9 is finite

thus F9 is finite by A20, TOPS_2:8; :: thesis: verum

end;( 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 A15, TOPS_2:10;

F <> {} by A14, TOPS_2:3;

then A17: G <> {} by TOPS_2:5;

meet G = (union F) ` by A14, TOPS_2:3, TOPS_2:6

.= ([#] T) \ ([#] T) by A14, SETFAM_1:45

.= {} by XBOOLE_1:37 ;

then not G is centered by A13, A16;

then consider G9 being set such that

A18: G9 <> {} and

A19: G9 c= G and

A20: G9 is finite and

A21: meet G9 = {} by A17, FINSET_1:def 3;

reconsider G9 = G9 as Subset-Family of T by A19, XBOOLE_1:1;

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

union F9 =
(meet G9) `
by A18, TOPS_2:7
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 A22, SETFAM_1:def 7;

then (A1 `) ` in F by A19, SETFAM_1:def 7;

hence A in F ; :: thesis: verum

end;assume A22: A in F9 ; :: thesis: A in F

then reconsider A1 = A as Subset of T ;

A1 ` in G9 by A22, SETFAM_1:def 7;

then (A1 `) ` in F by A19, SETFAM_1:def 7;

hence A in F ; :: thesis: verum

.= [#] T by A21 ;

hence F9 is Cover of T by SETFAM_1:def 11; :: thesis: F9 is finite

thus F9 is finite by A20, TOPS_2:8; :: thesis: verum