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