let X be BCK-Algebra_with_Condition(S); :: thesis: for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X
for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X

proof

let x, y, z be Element of X; :: thesis: ((x * y) \ (y * z)) \ (z * x) = 0. X
(y * x) \ y <= x by Lm2;
then A1: ((y * x) \ y) \ z <= x \ z by BCIALG_1:5;
x * y = y * x by Th6;
then (x * y) \ (y * z) <= x \ z by A1, Th11;
then A2: ((x * y) \ (y * z)) \ (z * x) <= (x \ z) \ (z * x) by BCIALG_1:5;
(x \ z) \ (z * x) = ((x \ z) \ z) \ x by Th11
.= ((x \ z) \ x) \ z by BCIALG_1:7
.= ((x \ x) \ z) \ z by BCIALG_1:7
.= (z `) \ z by BCIALG_1:def 5
.= z ` by BCIALG_1:def 8
.= 0. X by BCIALG_1:def 8 ;
then (((x * y) \ (y * z)) \ (z * x)) \ (0. X) = 0. X by A2;
hence ((x * y) \ (y * z)) \ (z * x) = 0. X by BCIALG_1:2; :: thesis: verum

end;

hence for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X ; :: thesis: verum