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
A1: B2 is_maximal_independent_in [#] M by Def12;
B1 is_maximal_independent_in [#] M by Def12;
hence card B1 = card B2 by A1, Th16; :: thesis: verum