theorem :: CARD_2:67

for n being Nat holds Rank n is finite