theorem Th31: :: HEYTING3:31

for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k}))
for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X