theorem :: CARD_4:24

for D being non empty set st not D is finite holds
card D = card (D *)