theorem :: NUMPOLY1:49

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