let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of T st F is all-closed-containing & F c= G holds
G is all-closed-containing
let F, G be Subset-Family of T; :: thesis: ( F is all-closed-containing & F c= G implies G is all-closed-containing )
assume that
A1: F is all-closed-containing and
A2: F c= G ; :: thesis: G is all-closed-containing
for A being Subset of T st A is closed holds
A in G

proof

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

end;

hence G is all-closed-containing by Def3; :: thesis: verum