set F = succ X;
X in {X} by TARSKI:def 1;
then X in succ X by XBOOLE_0:def 3;
then reconsider R1 = {[X,X]} as Relation of (succ X),(succ X) by RELSET_1:3;
A1: {X} c= succ X by XBOOLE_1:7;
A2: X c= succ X by XBOOLE_1:7;
[:{X},X:] c= [:{X},X:] ;
then reconsider R2 = [:{X},X:] as Relation of (succ X),(succ X) by A1, A2, RELSET_1:7;
reconsider R3 = R1 \/ R2 as Relation of (succ X),(succ X) ;
reconsider R4 = id X as Relation of (succ X),(succ X) by A2, RELSET_1:7;
R3 \/ R4 is Relation of (succ X),(succ X) ;
hence ({[X,X]} \/ [:{X},X:]) \/ (id X) is Relation of (succ X),(succ X) ; :: thesis: verum