theorem :: YELLOW_3:46

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