theorem Th36: :: HEYTING3:36

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