let X be BCI-algebra; ( 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
; 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;
( 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
;
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;
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; verum