theorem :: YELLOW_4:20

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