theorem Th12: :: WAYBEL_2:12

for L being non empty reflexive antisymmetric up-complete RelStr
for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))]