theorem Th22: :: BCIALG_6:22

for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)