let X be BCK-algebra; :: thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) :: thesis: ( ( for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) implies X is BCK-positive-implicative BCK-algebra )

proof

assume A1: X is BCK-positive-implicative BCK-algebra ; :: thesis: for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z
let x, y, z be Element of X; :: thesis: (x \ z) \ (y \ z) <= (x \ y) \ z
((x \ z) \ (y \ z)) \ ((x \ y) \ z) = ((x \ z) \ (y \ z)) \ ((x \ z) \ (y \ z)) by A1, Def11
.= 0. X by BCIALG_1:def 5 ;
hence (x \ z) \ (y \ z) <= (x \ y) \ z ; :: thesis: verum

end;

assume A2: for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ; :: thesis: X is BCK-positive-implicative BCK-algebra
for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ (y \ z)

proof

let x, y, z be Element of X; :: thesis: (x \ y) \ z = (x \ z) \ (y \ z)
(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 ;
then x \ y <= x \ (y \ z) by BCIALG_1:5;
then (x \ y) \ z <= (x \ (y \ z)) \ z by BCIALG_1:5;
then ((x \ y) \ z) \ ((x \ (y \ z)) \ z) = 0. X ;
then A3: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7;
(x \ z) \ (y \ z) <= (x \ y) \ z by A2;
then ((x \ z) \ (y \ z)) \ ((x \ y) \ z) = 0. X ;
hence (x \ y) \ z = (x \ z) \ (y \ z) by A3, BCIALG_1:def 7; :: thesis: verum

end;

hence X is BCK-positive-implicative BCK-algebra by Def11; :: thesis: verum