theorem :: GROUP_3:21

for G being Group
for a being Element of G holds
( a |^ (a ") = a & (a ") |^ a = a " ) by Th1;