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)

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

hence
X is BCI-algebra of 0 ,1,1,1
by Def3; :: thesis: verum
let x, y be Element of X; :: thesis: 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) ; :: thesis: verum

end;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) ; :: thesis: verum