let M be non void subset-closed finite-degree SubsetFamilyStr; :: thesis: for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C
let C be Subset of M; :: thesis: ex A being independent Subset of M st A is_maximal_independent_in C
{} M c= C ;
then ex A being independent Subset of M st
( {} M c= A & A is_maximal_independent_in C ) by Th14;
hence ex A being independent Subset of M st A is_maximal_independent_in C ; :: thesis: verum