theorem Th15: :: BINOP_1:15

for A being non empty set
for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o ) by Th13;