theorem :: HEYTING3:22

for n, k being Element of NAT holds not PFCrt (n,k) in PFBrt ((n + 1),k)