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 )

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

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 A2:
for x, y being Element of X holds x \ y = (x \ y) \ y
; :: thesis: X is BCK-positive-implicative BCK-algebra
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) \ y = (x \ y) \ (y \ y) by A1, Def11

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

.= x \ y by BCIALG_1:2 ;

hence x \ y = (x \ y) \ y ; :: thesis: verum

end;let x, y be Element of X; :: thesis: x \ y = (x \ y) \ y

(x \ y) \ y = (x \ y) \ (y \ y) by A1, Def11

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

.= x \ y by BCIALG_1:2 ;

hence x \ y = (x \ y) \ y ; :: thesis: verum

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

proof

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

(y \ z) \ y = (y \ y) \ z by BCIALG_1:7

.= z ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then y \ z <= y ;

then (x \ z) \ y <= (x \ z) \ (y \ z) by BCIALG_1:5;

then ((x \ z) \ y) \ ((x \ z) \ (y \ z)) = 0. X ;

then A3: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7;

((x \ z) \ (y \ z)) \ ((x \ y) \ z) = (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) by A2

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

.= 0. X by BCIALG_1:def 3 ;

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

end;(y \ z) \ y = (y \ y) \ z by BCIALG_1:7

.= z ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then y \ z <= y ;

then (x \ z) \ y <= (x \ z) \ (y \ z) by BCIALG_1:5;

then ((x \ z) \ y) \ ((x \ z) \ (y \ z)) = 0. X ;

then A3: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7;

((x \ z) \ (y \ z)) \ ((x \ y) \ z) = (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) by A2

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

.= 0. X by BCIALG_1:def 3 ;

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