let M be finite-degree Matroid; :: thesis: for B1, B2 being Basis of M holds card B1 = card B2
let B1, B2 be Basis of M; :: thesis: card B1 = card B2
( B1 is_maximal_independent_in [#] M & B2 is_maximal_independent_in [#] M ) by BASIS;
hence card B1 = card B2 by M3; :: thesis: verum