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