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