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 & {} M is independent ) by XBOOLE_1:2;
then ex A being independent Subset of M st
( {} M c= A & A is_maximal_independent_in C ) by Th;
hence ex A being independent Subset of M st A is_maximal_independent_in C ; :: thesis: verum