let M be non void subset-closed SubsetFamilyStr; :: thesis: for A being independent Subset of
for B being set st B c= A holds
B is independent Subset of
let A be independent Subset of ; :: thesis: for B being set st B c= A holds
B is independent Subset of
let B be set ; :: thesis: ( B c= A implies B is independent Subset of )
assume A1: B c= A ; :: thesis: B is independent Subset of
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 by Def2; :: thesis: verum