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)) = (0. X) \ (x \ y) )
A1: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. 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)) = (0. X) \ (x \ y) ; :: thesis: X is BCI-commutative
for x, y being Element of X st x \ y = 0. X holds
x = y \ (y \ x)

proof

let x, y be Element of X; :: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )
A3: (y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
assume A4: x \ y = 0. X ; :: thesis: x = y \ (y \ x)
then 0. X = (0. X) \ (x \ y) by BCIALG_1:2
.= (x \ (0. X)) \ (y \ (y \ x)) by A2, A4
.= x \ (y \ (y \ x)) by BCIALG_1:2 ;
hence x = y \ (y \ x) by A3, BCIALG_1:def 7; :: thesis: verum

end;

hence X is BCI-commutative ; :: thesis: verum

end;

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

proof

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

end;

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