theorem Th3: :: WAYBEL_3:3

for L being non empty Poset st ( L is with_suprema or L is /\-complete ) holds
for x, y, z being Element of L st x << z & y << z holds
( ex_sup_of {x,y},L & x "\/" y << z )