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 )

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

( (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 A3:
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) = 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;( (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

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

hence
X is associative BCI-algebra
by Th49; :: thesis: verum
A4:
for x, y being Element of X holds y \ x = x \ y

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;proof

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

then y \ (x `) = x \ y by A3;

hence y \ x = x \ y by A3; :: thesis: verum

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