theorem Th40: :: HEYTING3:40

for m being Element of NAT
for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds
a <> {{}}