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

end;

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

proof

let x, y be Element of X; :: thesis: (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) by A2;
then A3: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X ;
((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by BCIALG_1:10;
hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A3, BCIALG_1:def 7; :: thesis: verum

end;

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