for L being non empty RelStr
for X, Y being set st ex_inf_of X,L & ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than Y ) ) holds
"/\" (X,L) = "/\" (Y,L)