not 3 is trivial by NAT_2:def 1;
hence PolygonalNumbers 3 is Subset of NAT by Lm4; :: thesis: verum