theorem Th17: :: HEYTING3:17

for n, k being Element of NAT holds PFCrt (n,k) c< PFCrt ((n + 1),k)