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