let A be non empty set ; :: thesis: for o, o' being BinOp of A st o' is commutative holds
( o' is_distributive_wrt o iff o' is_right_distributive_wrt o )
let o, o' be BinOp of A; :: thesis: ( o' is commutative implies ( o' is_distributive_wrt o iff o' is_right_distributive_wrt o ) )
( o' is_right_distributive_wrt o iff for a, b, c being Element of A holds o' . (o . a,b),c = o . (o' . a,c),(o' . b,c) ) by Def10;
hence ( o' is commutative implies ( o' is_distributive_wrt o iff o' is_right_distributive_wrt o ) ) by Th25; :: thesis: verum