:: deftheorem defines Rnk MATROID0:def 12 :
for M being finite-degree Matroid holds Rnk M = Rnk ([#] M);