let X be set ; :: thesis: X in succ X
X in {X} by TARSKI:def 1;
hence X in succ X by XBOOLE_0:def 3; :: thesis: verum