theorem Th5: :: YELLOW10:5

for S, T being non empty antisymmetric lower-bounded RelStr
for D being Subset of [:S,T:] st ( [:S,T:] is complete or ex_sup_of D,[:S,T:] ) holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]