theorem Th4: :: HEYTING3:4

for m being Element of NAT
for X being non empty finite Subset of [:NAT,{m}:] holds
not for k being non zero Element of NAT holds [((2 * k) + 1),m] in X