n - 0 >= 1 by NAT_1:14;
then n - 1 >= 0 by XREAL_1:11;
hence CenterPolygon (s,n) is natural by INT_1:3; :: thesis: verum