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;