let T be set ; :: thesis: for F being Subset-Family of T holds

( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )

let F be Subset-Family of T; :: thesis: ( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )

for G being countable Subset-Family of T st G c= F holds

meet G in F

( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )

let F be Subset-Family of T; :: thesis: ( F is closed_for_countable_meets & F is compl-closed iff ( F is closed_for_countable_unions & F is compl-closed ) )

hereby :: thesis: ( F is closed_for_countable_unions & F is compl-closed implies ( F is closed_for_countable_meets & F is compl-closed ) )

assume A4:
( F is closed_for_countable_unions & F is compl-closed )
; :: thesis: ( F is closed_for_countable_meets & F is compl-closed )assume A1:
( F is closed_for_countable_meets & F is compl-closed )
; :: thesis: ( F is closed_for_countable_unions & F is compl-closed )

for G being countable Subset-Family of T st G c= F holds

union G in F

end;for G being countable Subset-Family of T st G c= F holds

union G in F

proof

hence
( F is closed_for_countable_unions & F is compl-closed )
by A1; :: thesis: verum
let G be countable Subset-Family of T; :: thesis: ( G c= F implies union G in F )

assume A2: G c= F ; :: thesis: union G in F

end;assume A2: G c= F ; :: thesis: union G in F

per cases
( G = {} or G <> {} )
;

end;

suppose
G <> {}
; :: thesis: union G in F

then reconsider G9 = G as non empty Subset-Family of T ;

( COMPLEMENT G9 c= F & COMPLEMENT G9 is countable ) by A1, A2, Th1, Th16;

then A3: meet (COMPLEMENT G9) in F by A1;

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

.= union G9 ;

hence union G in F by A1, A3; :: thesis: verum

end;( COMPLEMENT G9 c= F & COMPLEMENT G9 is countable ) by A1, A2, Th1, Th16;

then A3: meet (COMPLEMENT G9) in F by A1;

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

.= union G9 ;

hence union G in F by A1, A3; :: thesis: verum

for G being countable Subset-Family of T st G c= F holds

meet G in F

proof

hence
( F is closed_for_countable_meets & F is compl-closed )
by A4; :: thesis: verum
let G be countable Subset-Family of T; :: thesis: ( G c= F implies meet G in F )

assume A5: G c= F ; :: thesis: meet G in F

end;assume A5: G c= F ; :: thesis: meet G in F

per cases
( G = {} or G <> {} )
;

end;

suppose
G <> {}
; :: thesis: meet G in F

then reconsider G9 = G as non empty Subset-Family of T ;

( COMPLEMENT G9 c= F & COMPLEMENT G9 is countable ) by A4, A5, Th1, Th16;

then A6: union (COMPLEMENT G9) in F by A4;

(union (COMPLEMENT G9)) ` = ((meet G9) `) ` by TOPS_2:7

.= meet G9 ;

hence meet G in F by A4, A6; :: thesis: verum

end;( COMPLEMENT G9 c= F & COMPLEMENT G9 is countable ) by A4, A5, Th1, Th16;

then A6: union (COMPLEMENT G9) in F by A4;

(union (COMPLEMENT G9)) ` = ((meet G9) `) ` by TOPS_2:7

.= meet G9 ;

hence meet G in F by A4, A6; :: thesis: verum