let X be BCI-algebra; :: thesis: for x, y being Element of X holds Polynom (0,0,x,y) = x \ (x \ y)
let x, y be Element of X; :: thesis: Polynom (0,0,x,y) = x \ (x \ y)
Polynom (0,0,x,y) = (x,(x \ y)) to_power (0 + 1) by BCIALG_2:1
.= x \ (x \ y) by BCIALG_2:2 ;
hence Polynom (0,0,x,y) = x \ (x \ y) ; :: thesis: verum