let X be BCK-Algebra_with_Condition(S); :: thesis: ( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )
A1: ( X is implicative implies for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )

proof

assume A2: X is implicative ; :: thesis: for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x))
let x, y, z be Element of X; :: thesis: x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x))
A3: X is positive-implicative by A2, Th51;
then A4: x = (x \ z) * (x \ (x \ z)) by Th49;
X is commutative by A2, Th51;
then A5: x \ (y \ z) = ((x \ z) * (z \ (z \ x))) \ (y \ z) by A4, Def9;
A6: ((x \ z) \ (y \ z)) \ ((x \ y) \ z) = (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) by A3, Def11
.= (((x \ z) \ z) \ (y \ z)) \ ((x \ z) \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def 3 ;
(y \ z) \ y = (y \ y) \ z by BCIALG_1:7
.= z ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then y \ z <= y by BCIALG_1:def 11;
then (x \ z) \ y <= (x \ z) \ (y \ z) by BCIALG_1:5;
then ((x \ z) \ y) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:def 11;
then ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7;
then A7: (x \ y) \ z = (x \ z) \ (y \ z) by A6, BCIALG_1:def 7;
(z \ (z \ x)) \ (y \ z) = (z \ (y \ z)) \ (z \ x) by BCIALG_1:7
.= z \ (z \ x) by A2, Def15 ;
hence x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) by A3, A5, A7, Th47; :: thesis: verum

end;

( ( for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) implies X is implicative )

proof

assume A8: for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ; :: thesis: X is implicative
for x, y being Element of X holds x \ (y \ x) = x

proof

let x, y be Element of X; :: thesis: x \ (y \ x) = x
x \ (y \ x) = ((x \ y) \ x) * (x \ (x \ x)) by A8
.= ((x \ y) \ x) * (x \ (0. X)) by BCIALG_1:def 5
.= ((x \ y) \ x) * x by BCIALG_1:2
.= ((x \ x) \ y) * x by BCIALG_1:7
.= (y ` ) * x by BCIALG_1:def 5
.= (0. X) * x by BCIALG_1:def 8 ;
hence x \ (y \ x) = x by Th9; :: thesis: verum

end;

hence X is implicative by Def15; :: thesis: verum

end;

hence ( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) by A1; :: thesis: verum