theorem :: BCIALG_6:9

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