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

proof

assume A1: X is BCI-commutative ; :: thesis: for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z)
for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z)

proof

let x, y, z be Element of X; :: thesis: ( x <= y & x <= z implies x <= y \ (y \ z) )
assume ( x <= y & x <= z ) ; :: thesis: x <= y \ (y \ z)
then A2: ( x \ z = 0. X & x \ y = 0. X ) by BCIALG_1:def 11;
then A3: x = y \ (y \ x) by A1, Def4;
then x \ (y \ (y \ z)) = (y \ (y \ (y \ z))) \ (y \ x) by BCIALG_1:7
.= (y \ z) \ (y \ x) by BCIALG_1:8
.= 0. X by A2, A3, BCIALG_1:7 ;
hence x <= y \ (y \ z) by BCIALG_1:def 11; :: thesis: verum

end;

hence for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) ; :: thesis: verum

end;

assume A4: for x, y, z being Element of X st x <= y & x <= z holds
x <= y \ (y \ z) ; :: 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) )
assume x \ y = 0. X ; :: thesis: x = y \ (y \ x)
then A5: x <= y by BCIALG_1:def 11;
x \ x = 0. X by BCIALG_1:def 5;
then x <= x by BCIALG_1:def 11;
then x <= y \ (y \ x) by A4, A5;
then A6: x \ (y \ (y \ x)) = 0. X by BCIALG_1:def 11;
(y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
hence x = y \ (y \ x) by A6, BCIALG_1:def 7; :: thesis: verum

end;

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