let M be SubsetFamilyStr; :: thesis: ( M is finite-degree implies M is finite-membered )
assume M is finite-membered ; :: according to MATROID0:def 7 :: thesis: ( for n being Nat ex A being finite Subset of M st
( A is independent & not card A <= n ) or M is finite-membered )
hence ( for n being Nat ex A being finite Subset of M st
( A is independent & not card A <= n ) or M is finite-membered ) ; :: thesis: verum