theorem :: NUMPOLY1:28

for n, s being Nat holds Polygon (s,n) = (((n * (s - 2)) * (n - 1)) / 2) + n ;