theorem :: BCIALG_6:27

for X being BCI-algebra holds
( X is BCK-algebra iff for x being Element of X holds
( x is finite-period & ord x = 1 ) )