for X being set st X is natural-membered holds
X c= NAT by ORDINAL1:def 12;