let TS be set ; :: thesis: for F, G being Subset-Family of TS st F is with_proper_subsets & G c= F holds
G is with_proper_subsets
let F, G be Subset-Family of TS; :: thesis: ( F is with_proper_subsets & G c= F implies G is with_proper_subsets )
assume A1: ( F is with_proper_subsets & G c= F ) ; :: thesis: G is with_proper_subsets
assume not G is with_proper_subsets ; :: thesis: contradiction
then TS in G by Def6;
hence contradiction by A1, Def6; :: thesis: verum