:: deftheorem defines Polygon NUMPOLY1:def 3 :
for s, n being natural Number holds Polygon (s,n) = (((n ^2) * (s - 2)) - (n * (s - 4))) / 2;