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 )

( (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 )

( (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 A2:
for x, y, z being Element of X holds
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 by A1, Th49;

then (x \ y) \ (z \ x) = z \ y by A1, Th48;

then (x \ y) \ (x \ z) = z \ y by A1, Th48;

hence ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) by A1, Th48, Th49; :: thesis: verum

end;( (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 by A1, Th49;

then (x \ y) \ (z \ x) = z \ y by A1, Th48;

then (x \ y) \ (x \ z) = z \ y by A1, Th48;

hence ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) by A1, Th48, Th49; :: thesis: verum

( (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

hence
X is associative BCI-algebra
by Th50; :: thesis: verum
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

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

end;A3: for x, y being Element of X holds y \ x = x \ y

proof

( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x )
by A2;
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 \ (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

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