let X, Y be set ; :: thesis: ( X c= Y implies succRel X c= succRel Y )
assume A1: X c= Y ; :: thesis: succRel X c= succRel Y

now :: thesis: for x, y being object st [x,y] in succRel X holds
[x,y] in succRel Y

let x, y be object ; :: thesis: ( [x,y] in succRel X implies [x,y] in succRel Y )
reconsider a = x, b = y as set by TARSKI:1;
assume [x,y] in succRel X ; :: thesis: [x,y] in succRel Y
then [a,b] in succRel X ;
then ( a in X & b in X & b = succ a ) by Def1;
hence [x,y] in succRel Y by A1, Def1; :: thesis: verum

end;

hence succRel X c= succRel Y by RELAT_1:def 3; :: thesis: verum