let X be BCK-Algebra_with_Condition(S); ( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )
A1:
( X is implicative implies for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )
proof
assume A2:
X is
implicative
;
for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x))
then A3:
X is
positive-implicative
by Th50;
let x,
y,
z be
Element of
X;
x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x))
A4:
X is
commutative
by A2, Th50;
x = (x \ z) * (x \ (x \ z))
by A3, Th48;
then A5:
x \ (y \ z) = ((x \ z) * (z \ (z \ x))) \ (y \ z)
by A4;
(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 A6:
((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 A3
.=
(((x \ z) \ z) \ (y \ z)) \ ((x \ z) \ y)
by BCIALG_1:7
.=
0. X
by BCIALG_1:def 3
;
then A7:
(x \ y) \ z = (x \ z) \ (y \ z)
by A6, BCIALG_1:def 7;
(z \ (z \ x)) \ (y \ z) =
(z \ (y \ z)) \ (z \ x)
by BCIALG_1:7
.=
z \ (z \ x)
by A2
;
hence
x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x))
by A3, A5, A7, Th46;
verum
end;
( ( for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) implies X is implicative )
hence
( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) )
by A1; verum