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

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