let X be BCI-algebra; :: thesis: ( X is BCI-algebra of 0 ,1, 0 , 0 implies X is BCI-commutative BCI-algebra )
assume A1: X is BCI-algebra of 0 ,1, 0 , 0 ; :: thesis: X is BCI-commutative BCI-algebra
for x, y being Element of X st y \ x = 0. X holds
y = x \ (x \ y)

proof

let x, y be Element of X; :: thesis: ( y \ x = 0. X implies y = x \ (x \ y) )
Polynom (0,1,x,y) = Polynom (0,0,y,x) by A1, Def3;
then ((x,(x \ y)) to_power 1) \ (y \ x) = (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:2;
then (x \ (x \ y)) \ (y \ x) = (((y,(y \ x)) to_power 1),(x \ y)) to_power 0 by BCIALG_2:2;
then A2: (x \ (x \ y)) \ (y \ x) = (y,(y \ x)) to_power 1 by BCIALG_2:1;
assume y \ x = 0. X ; :: thesis: y = x \ (x \ y)
then (x \ (x \ y)) \ (0. X) = y \ (0. X) by A2, BCIALG_2:2;
then y = (x \ (x \ y)) \ (0. X) by BCIALG_1:2;
hence y = x \ (x \ y) by BCIALG_1:2; :: thesis: verum

end;

then for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x) ;
hence X is BCI-commutative BCI-algebra by BCIALG_3:def 4; :: thesis: verum