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