theorem Th14: :: MATROID0:14

for M being non void finite-degree SubsetFamilyStr
for C, A being Subset of M st A c= C & A is independent holds
ex B being independent Subset of M st
( A c= B & B is_maximal_independent_in C )