s >= 0 + 2 by NAT_2:29;
then A1: s - 2 >= 0 by XREAL_1:19;
Polygon (s,n) = ((s - 2) * (Triangle (n -' 1))) + n by Th49;
hence Polygon (s,n) is natural by INT_1:3, A1; :: thesis: verum