let M be SubsetFamilyStr; :: thesis: ( M is finite implies M is finite-degree )
assume the carrier of M is finite ; :: according to STRUCT_0:def 11 :: thesis: M is finite-degree
then reconsider X = the carrier of M as finite set ;
thus M is finite-membered :: according to MATROID0:def 7 :: thesis: ex n being Nat st
for A being finite Subset of M st A is independent holds
card A <= n
proof
let x be set ; :: according to FINSET_1:def 6,MATROID0:def 6 :: thesis: ( not x in the_family_of M or x is finite )
assume x in the_family_of M ; :: thesis: x is finite
then x c= X ;
hence x is finite ; :: thesis: verum
end;
take card X ; :: thesis: for A being finite Subset of M st A is independent holds
card A <= card X
let A be finite Subset of M; :: thesis: ( A is independent implies card A <= card X )
thus ( A is independent implies card A <= card X ) by NAT_1:43; :: thesis: verum