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 * y) \ z) \ (x \ z)) \ ((x * y) \ x) = 0. X by BCIALG_1:def 3;
then ((x * y) \ z) \ (x \ z) <= (x * y) \ x ;
then (((x * y) \ z) \ (x \ z)) \ z <= ((x * y) \ x) \ z by BCIALG_1:5;
then A3: ((((x * y) \ z) \ (x \ z)) \ z) \ (((x * y) \ x) \ z) = 0. X ;
(x * y) \ x <= y by Lm2;
then ((x * y) \ x) \ z <= y \ z by BCIALG_1:5;
then A4: (((x * y) \ x) \ z) \ (y \ z) = 0. X ;
(x * y) \ z = (x * y) \ (z * z) by A2, Th44
.= ((x * y) \ z) \ z by Th11 ;
then ((x * y) \ z) \ (x \ z) = (((x * y) \ z) \ (x \ z)) \ z by BCIALG_1:7;
then (((x * y) \ z) \ (x \ z)) \ (y \ z) = 0. X by A3, A4, BCIALG_1:3;
then A5: ((x * y) \ z) \ ((x \ z) * (y \ z)) = 0. X by Th11;
y <= x * y by Th37;
then y \ z <= (x * y) \ z by BCIALG_1:5;
then ((x * y) \ z) * (y \ z) <= ((x * y) \ z) * ((x * y) \ z) by Th7;
then A6: (((x * y) \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X ;
x <= x * y by Th37;
then x \ z <= (x * y) \ z by BCIALG_1:5;
then (x \ z) * (y \ z) <= ((x * y) \ z) * (y \ z) by Th7;
then ((x \ z) * (y \ z)) \ (((x * y) \ z) * (y \ z)) = 0. X ;
then ((x \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by A6, BCIALG_1:3;
then ((x \ z) * (y \ z)) \ ((x * y) \ z) = 0. X by A2, Th44;
hence (x * y) \ z = (x \ z) * (y \ z) by A5, 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 Th8;
x \ (x * x) = (x \ x) \ x by Th11
.= 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 Th44; :: 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