theorem :: BCIALG_2:32

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