let A be non empty set ; :: thesis: for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o )
let o, o9 be BinOp of A; :: thesis: ( o9 is commutative implies ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) )
assume A1: o9 is commutative ; :: thesis: ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o )
then ( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o ) by Th14;
hence ( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o ) by A1, Th15; :: thesis: verum