for L being RelStr
for X being set
for a being Element of L st a in X & ex_inf_of X,L holds
"/\" (X,L) <= a