:: deftheorem Def8 defines ord BCIALG_2:def 8 :
for X being BCI-algebra
for x being Element of X st x is nilpotent holds
for b₃ being non zero Nat holds
( b₃ = ord x iff ( ((0. X),x) to_power b₃ = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b₃ <= m ) ) );