theorem :: NUMPOLY1:54

for n being Nat holds (Triangle (n -' 1)) + (Triangle n) = n ^2