:: deftheorem defines polygonal NUMPOLY1:def 5 :
for x being object holds
( x is polygonal iff ex s being Nat st x is s -gonal );