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