theorem :: ORDINAL1:7

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