:: deftheorem Def5 defines ord BCIALG_6:def 5 :
for X being BCI-algebra
for x being Element of X st x is finite-period holds
for b₃ being Element of NAT holds
( b₃ = ord x iff ( x |^ b₃ in BCK-part X & b₃ <> 0 & ( for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
b₃ <= m ) ) );