theorem Th18: :: HEYTING3:18

for n, m, k being Element of NAT holds not PFArt (n,m) c= PFCrt (k,m)