:: deftheorem defines *' ROBBINS1:def 4 :
for L being non empty ComplLLattStr
for x, y being Element of L holds x *' y = ((x `) "\/" (y `)) ` ;