theorem :: NUMPOLY1:30

for s being Nat holds Polygon (s,2) = s ;