theorem Th32: :: HEYTING3:32

for n being Element of NAT
for a being Element of (SubstPoset (NAT,{n})) st {} in a holds
a = {{}}