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

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

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

take
card X
; :: thesis: for A being finite Subset of M st A is independent holds
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;assume x in the_family_of M ; :: thesis: x is finite

then x c= X ;

hence x is finite ; :: thesis: verum

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