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