{ (Polygon (s,n)) where n is Nat : verum } c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Polygon (s,n)) where n is Nat : verum } or x in NAT )
assume x in { (Polygon (s,n)) where n is Nat : verum } ; :: thesis: x in NAT
then ex n being Nat st x = Polygon (s,n) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

hence PolygonalNumbers s is Subset of NAT ; :: thesis: verum