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

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence {n,m} is finite Subset of NAT by ZFMISC_1:32; :: thesis: verum