let X, Y be set ; :: thesis: ( succ X = succ Y implies X = Y )
assume that
A1: succ X = succ Y and
A2: X <> Y ; :: thesis: contradiction
Y in X \/ {X} by A1, Th2;
then A3: ( Y in X or Y in {X} ) by XBOOLE_0:def 3;
X in Y \/ {Y} by A1, Th2;
then ( X in Y or X in {Y} ) by XBOOLE_0:def 3;
hence contradiction by A2, A3, TARSKI:def 1; :: thesis: verum