theorem Th29: :: BCIALG_6:29

for X being BCI-algebra
for x being Element of X
for m, n being Nat st x is finite-period & ord x = n holds
( x |^ m in BCK-part X iff n divides m )