theorem :: BCIALG_6:12

for X being BCI-algebra
for x being Element of X
for n being Nat st x in BCK-part X holds
x |^ (- n) = 0. X