let X be BCI-algebra; ( X is weakly-positive-implicative BCI-algebra implies X is BCI-algebra of 0 ,1,1,1 )
assume A1:
X is weakly-positive-implicative BCI-algebra
; X is BCI-algebra of 0 ,1,1,1
for x, y being Element of X holds Polynom (0,1,x,y) = Polynom (1,1,y,x)
proof
let x,
y be
Element of
X;
Polynom (0,1,x,y) = Polynom (1,1,y,x)
A2:
(x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)
by A1, BCIALG_1:85;
(
((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)) \ (y \ x)),
(x \ y))
to_power 1
by A2, BCIALG_2:2
.=
(
((y,(y \ x)) to_power 2),
(x \ y))
to_power 1
by BCIALG_2:3
;
hence
Polynom (
0,1,
x,
y)
= Polynom (1,1,
y,
x)
;
verum
end;
hence
X is BCI-algebra of 0 ,1,1,1
by Def3; verum