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 )

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)

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 A6:
for x, y, z being Element of X st x <= y & x <= z holds
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)

x <= y \ (y \ z) ; :: thesis: verum

end;x <= y \ (y \ z)

for x, y, z being Element of X st x <= y & x <= z holds

x <= y \ (y \ z)

proof

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

assume that

A2: x <= y and

A3: x <= z ; :: thesis: x <= y \ (y \ z)

A4: x \ z = 0. X by A3;

x \ y = 0. X by A2;

then A5: x = y \ (y \ x) by A1;

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 A4, A5, BCIALG_1:7 ;

hence x <= y \ (y \ z) ; :: thesis: verum

end;assume that

A2: x <= y and

A3: x <= z ; :: thesis: x <= y \ (y \ z)

A4: x \ z = 0. X by A3;

x \ y = 0. X by A2;

then A5: x = y \ (y \ x) by A1;

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 A4, A5, BCIALG_1:7 ;

hence x <= y \ (y \ z) ; :: thesis: verum

x <= y \ (y \ z) ; :: thesis: verum

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

hence
X is BCI-commutative
; :: thesis: verum
let x, y be Element of X; :: thesis: ( x \ y = 0. X implies x = y \ (y \ x) )

x \ x = 0. X by BCIALG_1:def 5;

then A7: x <= x ;

assume x \ y = 0. X ; :: thesis: x = y \ (y \ x)

then x <= y ;

then x <= y \ (y \ x) by A6, A7;

then A8: x \ (y \ (y \ x)) = 0. X ;

(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 A8, BCIALG_1:def 7; :: thesis: verum

end;x \ x = 0. X by BCIALG_1:def 5;

then A7: x <= x ;

assume x \ y = 0. X ; :: thesis: x = y \ (y \ x)

then x <= y ;

then x <= y \ (y \ x) by A6, A7;

then A8: x \ (y \ (y \ x)) = 0. X ;

(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 A8, BCIALG_1:def 7; :: thesis: verum