( i in NAT & j in NAT ) by ORDINAL1:def 13;
hence {i,j} is Subset of NAT by ZFMISC_1:38; :: thesis: verum