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)

x = y \ (y \ x) ;

hence X is BCI-commutative BCI-algebra by BCIALG_3:def 4; :: thesis: verum

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

then
for x, y being Element of X st x \ y = 0. X holds
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;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

x = y \ (y \ x) ;

hence X is BCI-commutative BCI-algebra by BCIALG_3:def 4; :: thesis: verum