:: deftheorem defines "/\" YELLOW_4:def 4 :
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 ) } ;