for n, k being Element of NAT holds [((2 * n) + 1),k] in PFCrt (n,k) by Def3;