theorem :: HEYTING3:2

for X being finite Subset of NAT holds
not for k being odd Element of NAT holds k in X