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

proof

assume A1: X is BCK-positive-implicative BCK-algebra ; :: thesis: for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y))
let x, y be Element of X; :: thesis: x \ y = (x \ y) \ (x \ (x \ y))
A2: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) by BCIALG_1:7
.= ((x \ y) \ (y `)) \ (x \ (x \ y)) by BCIALG_1:def 5
.= ((x \ y) \ (0. X)) \ (x \ (x \ y)) by BCIALG_1:def 8
.= (x \ y) \ (x \ (x \ y)) by BCIALG_1:2 ;
(x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8
.= (x \ y) \ (0. X) by BCIALG_1:def 5
.= x \ y by BCIALG_1:2 ;
hence x \ y = (x \ y) \ (x \ (x \ y)) by A1, A2, Th29; :: thesis: verum

end;

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

proof

let x, y be Element of X; :: thesis: x \ y = (x \ y) \ y
(x \ y) \ (x \ (x \ y)) = (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
hence x \ y = (x \ y) \ y by A3; :: thesis: verum

end;

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