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 ) )

hereby :: thesis: ( F is closed_for_countable_unions & F is compl-closed implies ( 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

proof

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

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

suppose G = {} ; :: thesis: union G in F

hence union G in F by A1, A2, SETFAM_1:1, ZFMISC_1:2; :: thesis: verum

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;

end;

end;

hence ( F is closed_for_countable_unions & F is compl-closed ) by A1; :: thesis: verum

end;

assume A4: ( F is closed_for_countable_unions & F is compl-closed ) ; :: thesis: ( F is closed_for_countable_meets & F is compl-closed )
for G being countable Subset-Family of T st G c= F holds
meet G in F

proof

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

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

suppose G = {} ; :: thesis: meet G in F

hence meet G in F by A4, A5, SETFAM_1:1, ZFMISC_1:2; :: thesis: verum

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;

end;

end;

hence ( F is closed_for_countable_meets & F is compl-closed ) by A4; :: thesis: verum