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

proof

assume A2: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; :: thesis: X is BCI-commutative
let x, y be Element of X; :: according to BCIALG_3:def 4 :: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
assume x \ y = 0. X ; :: thesis: x = y \ (y \ x)
then x \ (x \ y) = x by BCIALG_1:2;
hence x = y \ (y \ x) by A2; :: thesis: verum

end;

( X is BCI-commutative implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) )

proof

assume A3: X is BCI-commutative ; :: thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
let x, y be Element of X; :: thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y)))
(x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A3; :: thesis: verum

end;

hence ( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) by A1; :: thesis: verum