theorem Th16: :: HEYTING3:16

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