let X be BCI-algebra; ( 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 )
( 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
;
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;
Polynom (0,1,x,y) = Polynom (0,1,y,x)
(x \ y) \ (x \ y) = 0. X
by BCIALG_1:def 5;
then
(x \ (x \ y)) \ y = 0. X
by BCIALG_1:7;
then A2:
x \ (x \ y) <= y
;
x \ (x \ y) = (x \ (x \ y)) \ (x \ y)
by A1, BCIALG_3:28;
then
x \ (x \ y) <= y \ (x \ y)
by A2, BCIALG_1:5;
then
(x \ (x \ y)) \ (y \ x) <= (y \ (x \ y)) \ (y \ x)
by BCIALG_1:5;
then A3:
(x \ (x \ y)) \ (y \ x) <= (y \ (y \ x)) \ (x \ y)
by BCIALG_1:7;
(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
;
then A4:
(y \ (y \ x)) \ (y \ x) <= x \ (y \ x)
by BCIALG_1:5;
y \ (y \ x) = (y \ (y \ x)) \ (y \ x)
by A1, BCIALG_3:28;
then
(y \ (y \ x)) \ (x \ y) <= (x \ (y \ x)) \ (x \ y)
by A4, BCIALG_1:5;
then
(y \ (y \ x)) \ (x \ y) <= (x \ (x \ y)) \ (y \ x)
by BCIALG_1:7;
then A5:
(x \ (x \ y)) \ (y \ x) = (y \ (y \ x)) \ (x \ y)
by A3, Th2;
(
((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 A5, 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)
;
verum
end;
hence
X is
BCK-algebra of
0 ,1,
0 ,1
by A1, Def3;
verum
end;
assume A6:
X is BCK-algebra of 0 ,1, 0 ,1
; 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;
x \ y = (x \ y) \ y
A7:
Polynom (
0,1,
x,
(x \ y))
= Polynom (
0,1,
(x \ y),
x)
by A6, Def3;
A8:
(x \ y) \ x =
(x \ x) \ y
by BCIALG_1:7
.=
y `
by BCIALG_1:def 5
.=
0. X
by A6, BCIALG_1:def 8
;
then A9:
((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) =
(x \ y) \ (x \ (x \ y))
by BCIALG_1:2
.=
(x \ (x \ (x \ y))) \ y
by BCIALG_1:7
.=
(x \ y) \ y
by BCIALG_1:8
;
A10:
(x \ (x \ (x \ y))) \ ((x \ y) \ x) =
(x \ y) \ ((x \ y) \ x)
by BCIALG_1:8
.=
x \ y
by A8, BCIALG_1:2
;
(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 A7, 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
;
hence
x \ y = (x \ y) \ y
by A10, A9;
verum
end;
hence
X is BCK-positive-implicative BCK-algebra
by A6, BCIALG_3:28; verum