thus modRel 3 = (succRel 3) \/ {[(3 - 1),0]} by Th41
.= {[0,1],[1,2],[2,0]} by Th7, ENUMSET1:3 ; :: thesis: verum