let X be non empty BCIStr_0 ; :: thesis: ( X is BCI-algebra iff ( X is being_BCI-4 & ( for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )

thus ( X is BCI-algebra implies ( X is being_BCI-4 & ( for x, y, z being Element of X holds

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

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra )

thus ( X is being_BCI-4 & ( for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra ) :: thesis: verum

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) )

thus ( X is BCI-algebra implies ( X is being_BCI-4 & ( for x, y, z being Element of X holds

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

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra )

thus ( X is being_BCI-4 & ( for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra ) :: thesis: verum

proof

assume that

A1: X is being_BCI-4 and

A2: for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ; :: thesis: X is BCI-algebra

A3: X is being_I

end;A1: X is being_BCI-4 and

A2: for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ; :: thesis: X is BCI-algebra

A3: X is being_I

proof

let x be Element of X; :: according to BCIALG_1:def 5 :: thesis: x \ x = 0. X

x \ x = (x \ x) \ (0. X) by A2;

then x \ x = ((x \ (0. X)) \ x) \ (0. X) by A2;

then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) by A2;

then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) by A2;

hence x \ x = 0. X by A2; :: thesis: verum

end;x \ x = (x \ x) \ (0. X) by A2;

then x \ x = ((x \ (0. X)) \ x) \ (0. X) by A2;

then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) by A2;

then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) by A2;

hence x \ x = 0. X by A2; :: thesis: verum

now :: thesis: for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )

hence
X is BCI-algebra
by A1, A3, Th1; :: thesis: verum( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X )

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

((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) = 0. X by A2;

then (x \ (x \ y)) \ (y \ (0. X)) = 0. X by A2;

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

end;((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) = 0. X by A2;

then (x \ (x \ y)) \ (y \ (0. X)) = 0. X by A2;

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