theorem Th15: :: YELLOW_4:15

for L being non empty RelStr
for Y being Subset of L
for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y }