let X be BCI-algebra; :: thesis: ( X is positive-implicative BCI-algebra implies X is BCI-algebra of 0 ,1,1,1 )
assume A1: X is positive-implicative BCI-algebra ; :: thesis: 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; :: thesis: Polynom 0 ,1,x,y = Polynom 1,1,y,x
B1: (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 B1, 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 ; :: thesis: verum

end;

hence X is BCI-algebra of 0 ,1,1,1 by Def2; :: thesis: verum