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 )
x ` = 0. X by A1, BCIALG_1:def 8;
then 0. X <= x by BCIALG_1:def 11;
then x in BCK-part X ;
then A5: ( x |^ 1 in BCK-part X & 1 <> 0 ) by Th3;
then A3: x is finite-period by Defx1;
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 ( x |^ m in BCK-part X & m <> 0 ) ; :: thesis: 1 <= m
then 0 + 1 <= m by INT_1:20;
hence 1 <= m ; :: thesis: verum

end;

hence ( x is finite-period & ord x = 1 ) by A3, A5, Def8a; :: thesis: verum

end;

assume B1: 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
(y \ z) \ y = (y \ y) \ z by BCIALG_1:7;
then C1: (y \ z) \ y = z ` by BCIALG_1:def 5;
( z is finite-period & ord z = 1 ) by B1;
then z |^ 1 in BCK-part X by Def8a;
then z in BCK-part X by Th3;
then consider z1 being Element of X such that
D1: ( z = z1 & 0. X <= z1 ) ;
thus (y \ z) \ y = 0. X by D1, C1, BCIALG_1:def 11; :: thesis: verum

end;

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