:: deftheorem defines is_distributive_wrt BINOP_1:def 11 :
for A being set
for o9, o being BinOp of A holds
( o9 is_distributive_wrt o iff ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ) );