let X be natural-membered set ; :: thesis: addRel (X,1) = succRel X

now :: thesis: for x, y being object holds
( ( [x,y] in addRel (X,1) implies [x,y] in succRel X ) & ( [x,y] in succRel X implies [x,y] in addRel (X,1) ) )

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

hereby :: thesis: ( [x,y] in succRel X implies [x,y] in addRel (X,1) )

assume A1: [x,y] in addRel (X,1) ; :: thesis: [x,y] in succRel X
then [a,b] in addRel (X,1) ;
then ( a in X & b in X ) by MMLQUER2:4;
then reconsider a = a, b = b as Nat ;
[a,b] in addRel (X,1) by A1;
then A2: ( a in X & b in X & b = 1 + a ) by Th11;
then b = Segm (a + 1) by ORDINAL1:def 17
.= succ (Segm a) by NAT_1:38
.= succ a by ORDINAL1:def 17 ;
hence [x,y] in succRel X by A2, Def1; :: thesis: verum

end;

assume [x,y] in succRel X ; :: thesis: [x,y] in addRel (X,1)
then [a,b] in succRel X ;
then A3: ( a in X & b in X & b = succ a ) by Def1;
then reconsider a = a, b = b as Nat ;
b = succ (Segm a) by A3, ORDINAL1:def 17
.= Segm (a + 1) by NAT_1:38
.= 1 + a by ORDINAL1:def 17 ;
hence [x,y] in addRel (X,1) by A3, Th11; :: thesis: verum

end;

hence addRel (X,1) = succRel X by RELAT_1:def 2; :: thesis: verum