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