let X be quasi-commutative BCK-algebra; :: thesis: ( X is BCK-algebra of 0 ,1, 0 ,1 iff for x, y being Element of X holds x \ y = (x \ y) \ y )
thus
( X is BCK-algebra of 0 ,1, 0 ,1 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-algebra of 0 ,1, 0 ,1 )proof
assume A1:
X is
BCK-algebra of
0 ,1,
0 ,1
;
:: thesis: for x, y being Element of X holds x \ y = (x \ y) \ y
for
x,
y being
Element of
X holds
x \ y = (x \ y) \ y
proof
let x,
y be
Element of
X;
:: thesis: x \ y = (x \ y) \ y
B1:
Polynom 0 ,1,
x,
(x \ y) = Polynom 0 ,1,
(x \ y),
x
by A1, Def2;
B2:
(x \ (x \ (x \ y))) \ ((x \ y) \ x) =
(x,(x \ (x \ y)) to_power 1) \ ((x \ y) \ x)
by BCIALG_2:2
.=
((x \ y),((x \ y) \ x) to_power 1),
(x \ (x \ y)) to_power 1
by B1, BCIALG_2:2
.=
((x \ y) \ ((x \ y) \ x)),
(x \ (x \ y)) to_power 1
by BCIALG_2:2
.=
((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y))
by BCIALG_2:2
;
B3:
(x \ y) \ x =
(x \ x) \ y
by BCIALG_1:7
.=
y `
by BCIALG_1:def 5
.=
0. X
by BCIALG_1:def 8
;
B4:
(x \ (x \ (x \ y))) \ ((x \ y) \ x) =
(x \ y) \ ((x \ y) \ x)
by BCIALG_1:8
.=
x \ y
by B3, BCIALG_1:2
;
((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) =
(x \ y) \ (x \ (x \ y))
by B3, BCIALG_1:2
.=
(x \ (x \ (x \ y))) \ y
by BCIALG_1:7
.=
(x \ y) \ y
by BCIALG_1:8
;
hence
x \ y = (x \ y) \ y
by B2, B4;
:: thesis: verum
end;
hence
for
x,
y being
Element of
X holds
x \ y = (x \ y) \ y
;
:: thesis: verum
end;
assume
for x, y being Element of X holds x \ y = (x \ y) \ y
; :: thesis: X is BCK-algebra of 0 ,1, 0 ,1
then
X is BCK-positive-implicative BCK-algebra
by BCIALG_3:28;
hence
X is BCK-algebra of 0 ,1, 0 ,1
by Th46; :: thesis: verum