let X, Y be set ; :: thesis: ( succ X, succ Y are_equipotent implies X,Y are_equipotent )
A1: ( X in succ X & Y in succ Y ) by ORDINAL1:6;
( X = (succ X) \ {X} & Y = (succ Y) \ {Y} ) by ORDINAL1:37;
hence ( succ X, succ Y are_equipotent implies X,Y are_equipotent ) by A1, Th33; :: thesis: verum