:: deftheorem Def1 defines succRel RELSET_3:def 1 :
for X being set
for b₂ being Relation of X holds
( b₂ = succRel X iff for x, y being set holds
( [x,y] in b₂ iff ( x in X & y in X & y = succ x ) ) );