:: deftheorem defines finite-period BCIALG_6:def 4 :
for X being BCI-algebra
for x being Element of X holds
( x is finite-period iff ex n being Element of NAT st
( n <> 0 & x |^ n in BCK-part X ) );