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 )
proof
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
proof
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;
then X is being_BCI-4 ;
hence X is BCI-commutative BCI-algebra by A1, Th16, BCIALG_1:11; :: thesis: verum
end;
hence ( 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))) ) ) by Th16, BCIALG_1:1, BCIALG_1:2; :: thesis: verum