theorem Th8: :: WAYBEL20:8

for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]