for L being non empty RelStr
for X being set st ( ex_inf_of X,L or ex_sup_of X,L opp ) holds
"/\" (X,L) = "\/" (X,(L opp))