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 01: B c= A ; :: thesis: B is independent Subset of M
A in the_family_of M by Def8;
then B in the_family_of M by 01, CLASSES1:def 1;
hence B is independent Subset of M by Def8; :: thesis: verum