let n, m be Nat; :: thesis: {n,m} is finite Subset of NAT
( n in NAT & m in NAT ) by ORDINAL1:def 12;
hence {n,m} is finite Subset of NAT by ZFMISC_1:32; :: thesis: verum