theorem Th30: :: HEYTING3:30

for m being Element of NAT
for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds
for X being non empty set st X in a holds
ex n being Element of NAT st
( [n,m] in X & not n is odd )