let X be non empty BCIStr_0 ; :: thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) )
thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) :: thesis: ( ( for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra )

proof

assume A1: X is associative BCI-algebra ; :: thesis: for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
let x, y, z be Element of X; :: thesis: ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x )
(z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (y \ x)) \ (z \ x) by A1, Def20;
then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (y \ x) by A1, Th7;
then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (x \ y) by A1, Th48;
then A2: (z \ y) \ ((y \ x) \ (z \ x)) = 0. X by A1, Th1;
((y \ x) \ (z \ x)) \ (z \ y) = ((y \ x) \ (z \ x)) \ (y \ z) by A1, Th48;
then ((y \ x) \ (z \ x)) \ (z \ y) = 0. X by A1, Def3;
hence ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) by A1, A2, Def7, Th2; :: thesis: verum

end;

thus ( ( for x, y, z being Element of X holds
( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra ) :: thesis: verum

proof

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

proof

let x, y be Element of X; :: thesis: y \ x = x \ y
(y \ (0. X)) \ (x \ (0. X)) = x \ y by A3;
then y \ (x \ (0. X)) = x \ y by A3;
hence y \ x = x \ y by A3; :: thesis: verum

end;

( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) )

proof

A5: for a being Element of X holds a \ a = 0. X

proof

let a be Element of X; :: thesis: a \ a = 0. X
(a ` ) \ (a ` ) = (0. X) ` by A3;
then (a \ (0. X)) \ (a ` ) = (0. X) ` by A4;
then (a \ (0. X)) \ (a \ (0. X)) = (0. X) ` by A4;
then a \ a = (0. X) ` by A3;
hence a \ a = 0. X by A3; :: thesis: verum

end;

hence X is being_I by Def5; :: thesis: ( X is being_BCI-4 & ( for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) )
thus X is being_BCI-4 :: thesis: for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )

proof

for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
x = y

proof

let x, y be Element of X; :: thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y )
assume A6: ( x \ y = 0. X & y \ x = 0. X ) ; :: thesis: x = y
(x ` ) \ (y \ x) = y \ (0. X) by A3;
then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;
then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;
then x \ (x \ y) = y \ (0. X) by A3;
then y = x \ (x \ y) by A3
.= x by A3, A6 ;
hence x = y ; :: thesis: verum

end;

hence X is being_BCI-4 by Def7; :: thesis: verum

end;

thus for x, y, z being Element of X holds
( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) :: thesis: verum

proof

let x, y, z be Element of X; :: thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )
thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X :: thesis: (x \ (x \ y)) \ y = 0. X

proof

((x \ y) \ (x \ z)) \ (z \ y) = ((y \ x) \ (x \ z)) \ (z \ y) by A4
.= ((y \ x) \ (z \ x)) \ (z \ y) by A4
.= (z \ y) \ (z \ y) by A3 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A5; :: thesis: verum

end;

thus (x \ (x \ y)) \ y = 0. X :: thesis: verum

proof

(x ` ) \ (y \ x) = y \ (0. X) by A3;
then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4;
then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4;
then x \ (x \ y) = y \ (0. X) by A3;
then (x \ (x \ y)) \ y = y \ y by A3;
hence (x \ (x \ y)) \ y = 0. X by A5; :: thesis: verum

end;

end;

end;

then reconsider Y = X as BCI-algebra by Th1;
Y is associative by A4, Th48;
hence X is associative BCI-algebra ; :: thesis: verum

end;