let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds
( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )
let F be Subset-Family of T; :: thesis: ( F is all-closed-containing & F is compl-closed iff ( F is all-open-containing & F is compl-closed ) )

hereby :: thesis: ( F is all-open-containing & F is compl-closed implies ( F is all-closed-containing & F is compl-closed ) )

assume A1: ( F is all-closed-containing & F is compl-closed ) ; :: thesis: ( F is all-open-containing & F is compl-closed )
for A being Subset of T st A is open holds
A in F

proof

let A be Subset of T; :: thesis: ( A is open implies A in F )
assume A is open ; :: thesis: A in F
then A ` in F by A1;
then (A `) ` in F by A1;
hence A in F ; :: thesis: verum

end;

hence ( F is all-open-containing & F is compl-closed ) by A1; :: thesis: verum

end;

assume A2: ( F is all-open-containing & F is compl-closed ) ; :: thesis: ( F is all-closed-containing & F is compl-closed )
for A being Subset of T st A is closed holds
A in F

proof

let A be Subset of T; :: thesis: ( A is closed implies A in F )
assume A is closed ; :: thesis: A in F
then A ` in F by A2;
then (A `) ` in F by A2;
hence A in F ; :: thesis: verum

end;

hence ( F is all-closed-containing & F is compl-closed ) by A2; :: thesis: verum