let n, s be Nat; :: thesis: ( s >= 2 implies Polygon (s,n) is natural )
assume s >= 2 ; :: thesis: Polygon (s,n) is natural
then A1: s - 2 >= 2 - 2 by XREAL_1:9;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: Polygon (s,n) is natural

hence Polygon (s,n) is natural ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: Polygon (s,n) is natural

then n >= 0 + 1 by NAT_1:13;
then n - 1 >= 1 - 1 by XREAL_1:9;
then (((n * (s - 2)) * (n - 1)) / 2) + n >= 0 by A1;
hence Polygon (s,n) in NAT by INT_1:3; :: according to ORDINAL1:def 12 :: thesis: verum

end;

end;