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

proof

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

end;

hence G is all-open-containing by Def2; :: thesis: verum