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