let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is closed-domains-family holds
F is closed
let F be Subset-Family of T; :: thesis: ( F is closed-domains-family implies F is closed )
assume A1: F is closed-domains-family ; :: thesis: F is closed
for A being Subset of T st A in F holds
A is closed

proof

let A be Subset of T; :: thesis: ( A in F implies A is closed )
assume A in F ; :: thesis: A is closed
then A is closed_condensed by A1;
hence A is closed by TOPS_1:66; :: thesis: verum

end;

hence F is closed by TOPS_2:def 2; :: thesis: verum