theorem Th38: :: HEYTING3:38

for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & a = {{}} holds
b = {{}}