theorem :: NUMPOLY1:65

for n being non zero Nat holds ((Triangle (n -' 1)) + (6 * (Triangle n))) + (Triangle (n + 1)) = (8 * (Triangle n)) + 1