let A be independent Subset of M; :: thesis: A is finite
( A in the_family_of M & the_family_of M is finite-membered ) by Def7, Def8;
hence A is finite by Def6; :: thesis: verum