let X be BCI-algebra; :: thesis: for x being Element of X holds
( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )
let x be Element of X; :: thesis: ( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )
thus ( x is positive Element of X implies ( x is nilpotent & ord x = 1 ) ) :: thesis: ( x is nilpotent & ord x = 1 implies x is positive Element of X )

proof

assume x is positive Element of X ; :: thesis: ( x is nilpotent & ord x = 1 )
then 0. X <= x by Def2;
then A1: x ` = 0. X ;
thus A2: x is nilpotent :: thesis: ord x = 1

proof

set k = 1;
take 1 ; :: according to BCIALG_2:def 6 :: thesis: ((0. X),x) to_power 1 = 0. X
thus ((0. X),x) to_power 1 = 0. X by A1, Th2; :: thesis: verum

end;

thus ord x = 1 :: thesis: verum

proof

set k = 1;
reconsider k = 1 as non zero Nat ;
( ((0. X),x) to_power k = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m ) ) by A1, Th2, NAT_1:14;
hence ord x = 1 by A2, Def8; :: thesis: verum

end;

end;

assume ( x is nilpotent & ord x = 1 ) ; :: thesis: x is positive Element of X
then ((0. X),x) to_power 1 = 0. X by Def8;
then x ` = 0. X by Th2;
then 0. X <= x ;
hence x is positive Element of X by Def2; :: thesis: verum