let T be non empty TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:

hereby :: thesis:

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

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

end;

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

end;

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

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

end;

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