theorem :: NUMPOLY1:56

for n being non trivial Nat holds (1 / 3) * (Triangle ((3 * n) -' 1)) = (n * ((3 * n) - 1)) / 2