i in NAT by ORDINAL1:def 13;
hence {i} is Subset of NAT by ZFMISC_1:37; :: thesis: verum