for L being RelStr
for X, Y being set st X c= Y & ex_inf_of X,L & ex_inf_of Y,L holds
"/\" (X,L) >= "/\" (Y,L)