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