theorem Th34: :: CARD_1:35

for X, Y being set st succ X, succ Y are_equipotent holds
X,Y are_equipotent