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