:: deftheorem defines modRel RELSET_3:def 4 :
for n being non zero Nat holds modRel n = (addRel (n,1)) \/ {[(n - 1),0]};