:: deftheorem defines nilpotent BCIALG_2:def 7 :
for X being BCI-algebra holds
( X is nilpotent iff for x being Element of X holds x is nilpotent );