( n in NAT & k in NAT ) by ORDINAL1:def 12;
then [n,k] in [:NAT,NAT:] by ZFMISC_1:87;
hence In ([n,k],[:NAT,NAT:]) = [n,k] by SUBSET_1:def 8; :: thesis: verum