theorem Th25: :: GROUP_3:25

for G being Group
for a, b being Element of G holds
( (a |^ b) |^ (b ") = a & (a |^ (b ")) |^ b = a )