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