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

thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) :: thesis: ( ( for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) implies X is BCK-implicative BCK-algebra )

for x, y being Element of X holds x \ (y \ x) = x

thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) :: thesis: ( ( for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) implies X is BCK-implicative BCK-algebra )

proof

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

then A2: X is BCK-positive-implicative BCK-algebra by Th34;

for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z))

end;then A2: X is BCK-positive-implicative BCK-algebra by Th34;

for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z))

proof

hence
for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z))
; :: thesis: verum
let x, y, z be Element of X; :: thesis: x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z))

(x \ (0. X)) \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by A1, Th40;

then x \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2

.= (y \ z) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2 ;

then x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ x) by BCIALG_1:2

.= (y \ z) \ ((y \ x) \ z) by BCIALG_1:7 ;

hence x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) by A2, Def11; :: thesis: verum

end;(x \ (0. X)) \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by A1, Th40;

then x \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2

.= (y \ z) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2 ;

then x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ x) by BCIALG_1:2

.= (y \ z) \ ((y \ x) \ z) by BCIALG_1:7 ;

hence x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) by A2, Def11; :: thesis: verum

for x, y being Element of X holds x \ (y \ x) = x

proof

hence
X is BCK-implicative BCK-algebra
by Def12; :: thesis: verum
let x, y be Element of X; :: thesis: x \ (y \ x) = x

x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (x \ x)) by A3;

then x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (0. X)) by BCIALG_1:def 5;

then x \ (x \ (y \ x)) = (y \ x) \ (y \ x) by BCIALG_1:2;

then A4: x \ (x \ (y \ x)) = 0. X by BCIALG_1:def 5;

(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 ;

hence x \ (y \ x) = x by A4, BCIALG_1:def 7; :: thesis: verum

end;x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (x \ x)) by A3;

then x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (0. X)) by BCIALG_1:def 5;

then x \ (x \ (y \ x)) = (y \ x) \ (y \ x) by BCIALG_1:2;

then A4: x \ (x \ (y \ x)) = 0. X by BCIALG_1:def 5;

(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 ;

hence x \ (y \ x) = x by A4, BCIALG_1:def 7; :: thesis: verum