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

proof

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

proof

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

end;

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

end;

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

proof

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

proof

let x, z be Element of X; :: thesis: ( x \ z = 0. X implies x = z \ (z \ x) )
assume x \ z = 0. X ; :: thesis: x = z \ (z \ x)
then A5: x <= z by BCIALG_1:def 11;
set y = z \ (z \ x);
(z \ (z \ (z \ x))) \ (z \ x) = (z \ x) \ (z \ x) by BCIALG_1:8
.= 0. X by BCIALG_1:def 5 ;
then z \ (z \ (z \ x)) <= z \ x by BCIALG_1:def 11;
then x <= z \ (z \ x) by A4, A5;
then A6: x \ (z \ (z \ x)) = 0. X by BCIALG_1:def 11;
(z \ (z \ x)) \ x = (z \ x) \ (z \ x) by BCIALG_1:7
.= 0. X by BCIALG_1:def 5 ;
hence x = z \ (z \ x) by A6, BCIALG_1:def 7; :: thesis: verum

end;

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

end;

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