:: deftheorem defines PolygonalNumbers NUMPOLY1:def 9 :
for s being Nat holds PolygonalNumbers s = { (Polygon (s,n)) where n is Nat : verum } ;