0 is Element of NAT by ORDINAL2:19, SUBSET_1:def 2;