:: deftheorem Def1 defines terms've_same_card_as_number REARRAN1:def 1 :
for IT being FinSequence holds
( IT is terms've_same_card_as_number iff for n being Nat st 1 <= n & n <= len IT holds
for B being finite set st B = IT . n holds
card B = n );