reconsider n = n as Nat by TARSKI:1;
take n ; :: according to NUMPOLY1:def 4 :: thesis: Polygon (s,n) = Polygon (s,n)
thus Polygon (s,n) = Polygon (s,n) ; :: thesis: verum