:: deftheorem defines binop CAYLDICK:def 1 :
for D being set holds binop D = [:D,D:] --> the Element of D;