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

proof

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

end;

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

proof

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

end;

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