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) \ y )
thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ y <= (x \ y) \ y ) :: thesis: ( ( for x, y being Element of X holds x \ y <= (x \ y) \ 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) \ y
let x, y be Element of X; :: thesis: x \ y <= (x \ y) \ y
(x \ y) \ ((x \ y) \ y) = ((x \ y) \ y) \ ((x \ y) \ y) by A1, Th28
.= 0. X by BCIALG_1:def 5 ;
hence x \ y <= (x \ y) \ y ; :: thesis: verum

end;

assume A2: for x, y being Element of X holds x \ y <= (x \ y) \ 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 \ y) \ y by A2;
then A3: (x \ y) \ ((x \ y) \ y) = 0. X ;
((x \ y) \ y) \ (x \ y) = ((x \ y) \ (x \ y)) \ y by BCIALG_1:7
.= y ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
hence x \ y = (x \ y) \ y by A3, BCIALG_1:def 7; :: thesis: verum

end;

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