theorem :: NUMPOLY1:50
for n, s being Nat holds Polygon (s,n) = ((s - 3) * (Triangle (n -' 1))) + (Triangle n)