theorem Th43: :: WAYBEL_2:43

for L being non empty reflexive antisymmetric up-complete RelStr st inf_op L is directed-sups-preserving holds
for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)