assume not succRel X is empty ; :: thesis: contradiction
then consider z being object such that
A1: z in succRel X by XBOOLE_0:def 1;
consider x, y being object such that
A2: z = [x,y] by A1, RELAT_1:def 1;
reconsider a = x, b = y as set by TARSKI:1;
[a,b] in succRel X by A1, A2;
then A4: ( a in X & b in X & b = succ a ) by Def1;
then a = b by ZFMISC_1:def 10;
then b in b by A4, ORDINAL1:6;
hence contradiction ; :: thesis: verum