theorem Th39: :: HEYTING3:39

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