let X be non empty BCIStr_0 ; :: thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) )
thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x ` = x ) ) :: thesis: ( ( for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & 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
( (x \ y) \ (x \ z) = z \ y & x ` = x )
let x, y, z be Element of X; :: thesis: ( (x \ y) \ (x \ z) = z \ y & x ` = x )
(y \ x) \ (z \ x) = z \ y by A1, Th49;
then A2: (x \ y) \ (z \ x) = z \ y by A1, Th48;
x \ (0. X) = x by A1, Th49;
hence ( (x \ y) \ (x \ z) = z \ y & x ` = x ) by A1, A2, Th48; :: thesis: verum

end;

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

proof

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 `) \ (x `) = x \ y by A3;
then y \ (x `) = x \ y by A3;
hence y \ x = x \ y by A3; :: thesis: verum

end;

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

end;

hence X is associative BCI-algebra by Th49; :: thesis: verum