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

proof

assume A1: X is BCK-algebra ; :: thesis: for x being Element of X holds
( x is finite-period & ord x = 1 )
let x be Element of X; :: thesis: ( x is finite-period & ord x = 1 )
A2: for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
1 <= m

proof

let m be Element of NAT ; :: thesis: ( x |^ m in BCK-part X & m <> 0 implies 1 <= m )
assume that
x |^ m in BCK-part X and
A3: m <> 0 ; :: thesis: 1 <= m
0 + 1 <= m by A3, INT_1:7;
hence 1 <= m ; :: thesis: verum

end;

x ` = 0. X by A1, BCIALG_1:def 8;
then 0. X <= x ;
then x in BCK-part X ;
then A4: x |^ 1 in BCK-part X by Th4;
then x is finite-period ;
hence ( x is finite-period & ord x = 1 ) by A4, A2, Def5; :: thesis: verum

end;

assume A5: for x being Element of X holds
( x is finite-period & ord x = 1 ) ; :: thesis: X is BCK-algebra
for y, z being Element of X holds (y \ z) \ y = 0. X

proof

let y, z be Element of X; :: thesis: (y \ z) \ y = 0. X
( z is finite-period & ord z = 1 ) by A5;
then z |^ 1 in BCK-part X by Def5;
then z in BCK-part X by Th4;
then A6: ex z1 being Element of X st
( z = z1 & 0. X <= z1 ) ;
(y \ z) \ y = (y \ y) \ z by BCIALG_1:7;
then (y \ z) \ y = z ` by BCIALG_1:def 5;
hence (y \ z) \ y = 0. X by A6; :: thesis: verum

end;

then X is being_K ;
hence X is BCK-algebra by BCIALG_1:18; :: thesis: verum