theorem Th30: :: GROUP_3:30
for G being Group st ( for a, b being Element of G holds a |^ b = a ) holds
G is commutative