let M be non void subset-closed SubsetFamilyStr; :: thesis: for A being independent Subset of M
for B being set st B c= A holds
B is independent Subset of M
let A be independent Subset of M; :: thesis: for B being set st B c= A holds
B is independent Subset of M
let B be set ; :: thesis: ( B c= A implies B is independent Subset of M )
assume A1: B c= A ; :: thesis: B is independent Subset of M
A in the_family_of M by Def2;
then B in the_family_of M by A1, CLASSES1:def 1;
hence B is independent Subset of M by Def2; :: thesis: verum