:: deftheorem defines |^ GROUP_3:def 2 :
for G being Group
for a, b being Element of G holds a |^ b = ((b ") * a) * b;