:: deftheorem defines nilpotent BCIALG_2:def 6 :
for X being BCI-algebra
for x being Element of X holds
( x is nilpotent iff ex k being non zero Nat st ((0. X),x) to_power k = 0. X );