for n, k being Element of NAT holds PFCrt (n,k) misses {[((2 * n) + 3),k]}