for X being BCI-algebra
for x being Element of X holds
( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )