for M being non void subset-closed finite-degree SubsetFamilyStr
for C being Subset of M ex A being independent Subset of M st A is_maximal_independent_in C