:: deftheorem defines absorbs LATTICE2:def 1 :
for D being non empty set
for o, o9 being BinOp of D holds
( o absorbs o9 iff for x, y being Element of D holds o . (x,(o9 . (x,y))) = x );