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