defpred S₁[ object , object ] means $2 = succ (Segm $1);
consider R being Relation of X such that
A1: for x, y being object holds
( [x,y] in R iff ( x in X & y in X & S₁[x,y] ) ) from RELSET_1:sch 1();
take R ; :: thesis: for x, y being set holds
( [x,y] in R iff ( x in X & y in X & y = succ x ) )
let x, y be set ; :: thesis: ( [x,y] in R iff ( x in X & y in X & y = succ x ) )

hereby :: thesis: ( x in X & y in X & y = succ x implies [x,y] in R )

assume [x,y] in R ; :: thesis: ( x in X & y in X & y = succ x )
then ( x in X & y in X & S₁[x,y] ) by A1;
hence ( x in X & y in X & y = succ x ) by ORDINAL1:def 17; :: thesis: verum

end;

assume ( x in X & y in X & y = succ x ) ; :: thesis: [x,y] in R
then ( x in X & y in X & S₁[x,y] ) by ORDINAL1:def 17;
hence [x,y] in R by A1; :: thesis: verum