theorem Th42: :: YELLOW_4:42

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 }