theorem :: YELLOW_4:46

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