for L being non empty RelStr
for x, y, z being Element of L holds {x} "/\" {y,z} = {(x "/\" y),(x "/\" z)} by Lm4;