let X be non empty BCIStr_0 ; :: thesis: ( X is BCI-commutative BCI-algebra iff for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) )

( ( for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ) implies X is BCI-commutative BCI-algebra )

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ) by Th16, BCIALG_1:1, BCIALG_1:2; :: thesis: verum

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) )

( ( for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ) implies X is BCI-commutative BCI-algebra )

proof

hence
( X is BCI-commutative BCI-algebra iff for x, y, z being Element of X holds
assume A1:
for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ; :: thesis: X is BCI-commutative BCI-algebra

for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds

x = y

hence X is BCI-commutative BCI-algebra by A1, Th16, BCIALG_1:11; :: thesis: verum

end;( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ; :: thesis: X is BCI-commutative BCI-algebra

for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds

x = y

proof

then
X is being_BCI-4
;
let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )

assume that

A2: x \ y = 0. X and

A3: y \ x = 0. X ; :: thesis: x = y

A4: x \ (x \ y) = x by A1, A2;

y \ (y \ (x \ (x \ y))) = y \ (0. X) by A1, A2, A3

.= y by A1 ;

hence x = y by A1, A4; :: thesis: verum

end;assume that

A2: x \ y = 0. X and

A3: y \ x = 0. X ; :: thesis: x = y

A4: x \ (x \ y) = x by A1, A2;

y \ (y \ (x \ (x \ y))) = y \ (0. X) by A1, A2, A3

.= y by A1 ;

hence x = y by A1, A4; :: thesis: verum

hence X is BCI-commutative BCI-algebra by A1, Th16, BCIALG_1:11; :: thesis: verum

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ) by Th16, BCIALG_1:1, BCIALG_1:2; :: thesis: verum