theorem Th61: :: WAYBEL_1:61

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