for G being Group
for a, b being Element of G holds
( a |^ b = a iff a * b = b * a )