let A be independent Subset of ; :: 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