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

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