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 by BCIALG_1:def 11;
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 empty Element of NAT ;
A3: (0. X),x to_power k = 0. X by A1, Th2;
for m being Element of NAT st (0. X),x to_power m = 0. X & m <> 0 holds
k <= m by NAT_1:14;
hence ord x = 1 by A2, A3, 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 by BCIALG_1:def 11;
hence x is positive Element of X by Def2; :: thesis: verum