for n being Nat holds
( n is finite & card n is finite )