:: deftheorem defines "\/" YELLOW_4:def 3 :
for L being non empty RelStr
for D1, D2 being Subset of L holds D1 "\/" D2 = { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;