set n = 0 ;
Polygon (s,0) in { (Polygon (s,n)) where n is Nat : verum } ;
then PolygonalNumbers s <> {} ;
hence not PolygonalNumbers s is empty ; :: thesis: verum