theorem Th10: :: BCIALG_6:10

for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a `) |^ n = a |^ (- n)