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

end;

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

proof

let x, y, z be Element of X; :: thesis: ( (x \ y) \ (x \ z) = z \ y & x ` = x )
A3: 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
(x \ (0. X)) \ (x \ (0. X)) = (0. X) ` by A2;
then x \ (x \ (0. X)) = (0. X) ` by A2;
then x \ x = (0. X) ` by A2;
then A4: x \ x = 0. X by A2;
(x \ y) \ (x \ x) = y \ x by A2;
hence y \ x = x \ y by A2, A4; :: thesis: verum

end;

( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) by A2;
hence ( (x \ y) \ (x \ z) = z \ y & x ` = x ) by A3; :: thesis: verum

end;

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