let X be BCI-Algebra_with_Condition(S); :: thesis: for x, y being Element of X holds x * y = y * x
let x, y be Element of X; :: thesis: x * y = y * x
(y * x) \ y <= x by Lm2;
then ((y * x) \ y) \ x = 0. X ;
then ((y * x) \ x) \ y = 0. X by BCIALG_1:7;
then (y * x) \ x <= y ;
then y * x <= x * y by Lm2;
then A1: (y * x) \ (x * y) = 0. X ;
(x * y) \ x <= y by Lm2;
then ((x * y) \ x) \ y = 0. X ;
then ((x * y) \ y) \ x = 0. X by BCIALG_1:7;
then (x * y) \ y <= x ;
then x * y <= y * x by Lm2;
then (x * y) \ (y * x) = 0. X ;
hence x * y = y * x by A1, BCIALG_1:def 7; :: thesis: verum