:: deftheorem defines CenterPolygon NUMPOLY1:def 7 :
for s, n being Nat holds CenterPolygon (s,n) = (((s * n) / 2) * (n - 1)) + 1;