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

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

thus ( X is positive-implicative BCI-algebra implies for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) by Lm24, Th1, Th2, Th84; :: thesis: ( ( for x, y, z being Element of X holds

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

assume A1: for x, y, z being Element of X holds

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

hence X is positive-implicative BCI-algebra by Lm25; :: thesis: verum

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

thus ( X is positive-implicative BCI-algebra implies for x, y, z being Element of X holds

( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) by Lm24, Th1, Th2, Th84; :: thesis: ( ( for x, y, z being Element of X holds

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

assume A1: for x, y, z being Element of X holds

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

now :: thesis: for x being Element of X holds x \ x = 0. X

then A2:
X is being_I
;let x be Element of X; :: thesis: x \ x = 0. X

((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) = 0. X by A1;

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

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

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

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

end;((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) = 0. X by A1;

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

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

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

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

now :: thesis: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds

x = y

then A3:
X is being_BCI-4
;x = y

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

assume ( x \ y = 0. X & y \ x = 0. X ) ; :: thesis: x = y

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

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

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

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

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

hence x = y by A1; :: thesis: verum

end;assume ( x \ y = 0. X & y \ x = 0. X ) ; :: thesis: x = y

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

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

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

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

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

hence x = y by A1; :: 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 )

then
X is weakly-positive-implicative BCI-algebra
by A1, A2, A3, Th1, Th84;( ((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 )

thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; :: thesis: (x \ (x \ y)) \ y = 0. X

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

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

hence (x \ (x \ y)) \ y = 0. X by A1; :: thesis: verum

end;thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; :: thesis: (x \ (x \ y)) \ y = 0. X

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

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

hence (x \ (x \ y)) \ y = 0. X by A1; :: thesis: verum

hence X is positive-implicative BCI-algebra by Lm25; :: thesis: verum