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

proof

assume A2: X is positive-implicative ; :: thesis: for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z)
let x, y, z be Element of X; :: thesis: (x * y) \ z = (x \ z) * (y \ z)
( x <= x * y & y <= x * y ) by Th38;
then ( x \ z <= (x * y) \ z & y \ z <= (x * y) \ z ) by BCIALG_1:5;
then ( (x \ z) * (y \ z) <= ((x * y) \ z) * (y \ z) & ((x * y) \ z) * (y \ z) <= ((x * y) \ z) * ((x * y) \ z) ) by Th8;
then ( ((x \ z) * (y \ z)) \ (((x * y) \ z) * (y \ z)) = 0. X & (((x * y) \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X ) by BCIALG_1:def 11;
then ((x \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by BCIALG_1:3;
then A3: ((x \ z) * (y \ z)) \ ((x * y) \ z) = 0. X by A2, Th45;
A4: (x * y) \ z = (x * y) \ (z * z) by A2, Th45
.= ((x * y) \ z) \ z by Th12 ;
(((x * y) \ z) \ (x \ z)) \ ((x * y) \ x) = 0. X by BCIALG_1:def 3;
then ((x * y) \ z) \ (x \ z) <= (x * y) \ x by BCIALG_1:def 11;
then (((x * y) \ z) \ (x \ z)) \ z <= ((x * y) \ x) \ z by BCIALG_1:5;
then A5: ((((x * y) \ z) \ (x \ z)) \ z) \ (((x * y) \ x) \ z) = 0. X by BCIALG_1:def 11;
(x * y) \ x <= y by Lm2;
then ((x * y) \ x) \ z <= y \ z by BCIALG_1:5;
then A6: (((x * y) \ x) \ z) \ (y \ z) = 0. X by BCIALG_1:def 11;
((x * y) \ z) \ (x \ z) = (((x * y) \ z) \ (x \ z)) \ z by A4, BCIALG_1:7;
then (((x * y) \ z) \ (x \ z)) \ (y \ z) = 0. X by A5, A6, BCIALG_1:3;
then ((x * y) \ z) \ ((x \ z) * (y \ z)) = 0. X by Th12;
hence (x * y) \ z = (x \ z) * (y \ z) by A3, BCIALG_1:def 7; :: thesis: verum

end;

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

proof

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

proof

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

end;

hence X is positive-implicative by Th45; :: thesis: verum

end;

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