for L being non empty RelStr
for X being set st ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) holds
"/\" (X,L) = "/\" ((X /\ the carrier of L),L)