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

for A being Subset of T st A is closed holds

A in F

( 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 A2:
( F is all-open-containing & F is compl-closed )
; :: thesis: ( 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

end;for A being Subset of T st A is open holds

A in F

proof

hence
( F is all-open-containing & F is compl-closed )
by A1; :: thesis: verum
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;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

for A being Subset of T st A is closed holds

A in F

proof

hence
( F is all-closed-containing & F is compl-closed )
by A2; :: thesis: verum
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;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