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)
; verum