theorem Th14: :: BINOP_1:14

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_left_distributive_wrt o ) by Th12;