theorem Th12: :: WAYBEL14:12

for P being with_suprema Poset
for x, y being Element of P holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)