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