theorem :: BCIALG_6:11

for X being BCI-algebra
for x being Element of X
for n being Nat st x in BCK-part X & n >= 1 holds
x |^ n = x