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

hereby :: thesis:

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

let G be countable Subset-Family of T; :: thesis:
assume A2: G c= F ; :: thesis:

suppose G = {} ; :: thesis:

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

end;

suppose G <> {} ; :: thesis:

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:

end;

end;

end;

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

end;

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

let G be countable Subset-Family of T; :: thesis:
assume A5: G c= F ; :: thesis:

suppose G = {} ; :: thesis:

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

end;

suppose G <> {} ; :: thesis:

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:

end;

end;

end;

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