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:
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
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 () in F by A1;
(meet ()) ` = ((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:
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 ; :: 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 () in F by A4;
(union ()) ` = ((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