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