:: deftheorem defines \+\ YELLOW_5:def 2 :
for L being non empty RelStr
for a, b being Element of L holds a \+\ b = (a \ b) "\/" (b \ a);