theorem Th37: :: HEYTING3:37

for k being Element of NAT holds Bottom (SubstPoset (NAT,{k})) = {}