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 )

( ord x = 1 & x is nilpotent ) ; :: thesis: X is BCK-algebra

( 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

assume A5:
for x being Element of X holds
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 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

( ord x = 1 & x is nilpotent ) ; :: thesis: X is BCK-algebra

now :: thesis: for x being Element of X holds x ` = 0. X

hence
X is BCK-algebra
by BCIALG_1:def 8; :: thesis: verumlet 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;( 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