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