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 \ y) = y \ (y \ (x \ (x \ y))) )

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

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

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

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

proof

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

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

X is commutative BCK-algebra by A1, Th34;

then y \ (y \ (x \ (x \ y))) = y \ (y \ (y \ (y \ x))) by Def1

.= y \ (y \ x) by BCIALG_1:8 ;

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A1, Th35; :: thesis: verum

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

X is commutative BCK-algebra by A1, Th34;

then y \ (y \ (x \ (x \ y))) = y \ (y \ (y \ (y \ x))) by Def1

.= y \ (y \ x) by BCIALG_1:8 ;

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A1, Th35; :: thesis: verum

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

proof

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

A4: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8

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

.= x \ y by BCIALG_1:2 ;

(x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:8

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

.= (x \ y) \ y by BCIALG_1:8 ;

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

end;A4: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8

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

.= x \ y by BCIALG_1:2 ;

(x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:8

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

.= (x \ y) \ y by BCIALG_1:8 ;

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

proof

then A5:
X is commutative BCK-algebra
by Th4;
let x, y be Element of X; :: thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y)))

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

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

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

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

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

proof

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

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

.= y \ (y \ (y \ (y \ x))) by A5, Def1 ;

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by BCIALG_1:8; :: thesis: verum

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

.= y \ (y \ (y \ (y \ x))) by A5, Def1 ;

hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by BCIALG_1:8; :: thesis: verum