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

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