theorem Th72: :: NUMPOLY1:72

for n being Nat holds (n + 1) choose 2 = (n * (n + 1)) / 2