let A be independent Subset of M; :: thesis: A is finite
A1: the_family_of M is finite-membered by Def5;
A in the_family_of M by Def2;
hence A is finite by A1; :: thesis: verum