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