theorem Th16: :: CARD_1:17

for X, Y being set st X,Y are_equipotent holds
nextcard X = nextcard Y