thus ReciTriangRS . 0 = 1 / (Triangle 0) by Def13
.= 0 ; :: thesis: verum