theorem Th21: :: NUMPOLY1:21

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