theorem Th15: :: HEYTING3:15

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