A1: Polygon (s,0) is set ;
for n being Nat holds Polygon (s,n) in PolygonalNumbers s ;
hence not PolygonalNumbers s is empty by A1, XBOOLE_0:def 1; :: thesis: verum