let R1, R2 be Relation of X; :: thesis: ( ( for x, y being set holds
( [x,y] in R1 iff ( x in X & y in X & y = succ x ) ) ) & ( for x, y being set holds
( [x,y] in R2 iff ( x in X & y in X & y = succ x ) ) ) implies R1 = R2 )
assume that
A2: for x, y being set holds
( [x,y] in R1 iff ( x in X & y in X & y = succ x ) ) and
A3: for x, y being set holds
( [x,y] in R2 iff ( x in X & y in X & y = succ x ) ) ; :: thesis: R1 = R2

now :: thesis: for x, y being object holds
( ( [x,y] in R1 implies [x,y] in R2 ) & ( [x,y] in R2 implies [x,y] in R1 ) )

let x, y be object ; :: thesis: ( ( [x,y] in R1 implies [x,y] in R2 ) & ( [x,y] in R2 implies [x,y] in R1 ) )
reconsider a = x, b = y as set by TARSKI:1;

hereby :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

assume [x,y] in R1 ; :: thesis: [x,y] in R2
then [a,b] in R1 ;
then ( a in X & b in X & b = succ a ) by A2;
hence [x,y] in R2 by A3; :: thesis: verum

end;

assume [x,y] in R2 ; :: thesis: [x,y] in R1
then [a,b] in R2 ;
then ( a in X & b in X & b = succ a ) by A3;
hence [x,y] in R1 by A2; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum