let X be BCI-algebra; :: thesis: ( X is associative BCI-algebra implies ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) )
assume A1: X is associative BCI-algebra ; :: thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 )
for x being Element of X holds (x ` ) ` = x

proof

let x be Element of X; :: thesis: (x ` ) ` = x
x ` = x by A1, BCIALG_1:47;
hence (x ` ) ` = x ; :: thesis: verum

end;

then A2: X is p-Semisimple by BCIALG_1:54;
for x, y being Element of X holds Polynom 1,0 ,x,y = Polynom 0 ,0 ,y,x

proof

let x, y be Element of X; :: thesis: Polynom 1,0 ,x,y = Polynom 0 ,0 ,y,x
x \ (x \ y) = y by A2, BCIALG_1:def 26;
then A3: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, BCIALG_1:48;
(x,(x \ y) to_power (1 + 1)),(y \ x) to_power 0 = x,(x \ y) to_power 2 by BCIALG_2:1
.= (x \ (x \ y)) \ (x \ y) by BCIALG_2:3
.= y,(y \ x) to_power 1 by A3, BCIALG_2:2
.= (y,(y \ x) to_power 1),(x \ y) to_power 0 by BCIALG_2:1 ;
hence Polynom 1,0 ,x,y = Polynom 0 ,0 ,y,x ; :: thesis: verum

end;

hence ( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 ) by A2, Def3, Th42; :: thesis: verum