let X be BCI-algebra; :: thesis: ( X is BCK-algebra iff for x being Element of X holds
( ord x = 1 & x is nilpotent ) )
thus ( X is BCK-algebra implies for x being Element of X holds
( ord x = 1 & x is nilpotent ) ) :: thesis: ( ( for x being Element of X holds
( ord x = 1 & x is nilpotent ) ) implies X is BCK-algebra )
proof
set k = 1;
assume A1: X is BCK-algebra ; :: thesis: for x being Element of X holds
( ord x = 1 & x is nilpotent )
let x be Element of X; :: thesis: ( ord x = 1 & x is nilpotent )
A2: x ` = 0. X by A1, BCIALG_1:def 8;
then ((0. X),x) to_power 1 = 0. X by Th2;
then A3: x is nilpotent ;
reconsider k = 1 as non zero Nat ;
A4: for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
k <= m by NAT_1:14;
((0. X),x) to_power k = 0. X by A2, Th2;
hence ( ord x = 1 & x is nilpotent ) by A3, A4, Def8; :: thesis: verum
end;
assume A5: for x being Element of X holds
( ord x = 1 & x is nilpotent ) ; :: thesis: X is BCK-algebra
now :: thesis: for x being Element of X holds x ` = 0. X
let x be Element of X; :: thesis: x ` = 0. X
( ord x = 1 & x is nilpotent ) by A5;
then ((0. X),x) to_power 1 = 0. X by Def8;
hence x ` = 0. X by Th2; :: thesis: verum
end;
hence X is BCK-algebra by BCIALG_1:def 8; :: thesis: verum