let X be set ; :: thesis: X <> succ X
assume A1: X = succ X ; :: thesis: contradiction
X in succ X by Th2;
hence contradiction by A1; :: thesis: verum