let X be BCI-algebra; :: thesis: ( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) )
thus ( X is weakly-positive-implicative implies for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) :: thesis: ( ( for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) implies X is weakly-positive-implicative )

proof

assume A1: X is weakly-positive-implicative ; :: thesis: for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `)
let x, y be Element of X; :: thesis: x \ y = ((x \ y) \ y) \ (y `)
(x \ (0. X)) \ y = ((x \ y) \ y) \ (y `) by A1;
hence x \ y = ((x \ y) \ y) \ (y `) by Th2; :: thesis: verum

end;

assume A2: for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ; :: thesis: X is weakly-positive-implicative
for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z)

proof

let x, y, z be Element of X; :: thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z)
((x \ z) \ (y \ z)) \ (x \ y) = 0. X by Def3;
then (((x \ z) \ (y \ z)) \ z) \ ((x \ y) \ z) = 0. X by Th4;
then A3: (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) = 0. X by Th7;
(((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (y \ z) = 0. X by Th1;
then ((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ ((y \ z) \ (z `)) = 0. X by Th4;
then (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (((y \ z) \ (z `)) \ y) = 0. X by Th4;
then (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (((y \ z) \ (z `)) \ (y \ (0. X))) = 0. X by Th2;
then A4: (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (0. X) = 0. X by Def3;
((x \ y) \ z) \ (((x \ z) \ z) \ (y \ z)) = ((x \ z) \ y) \ (((x \ z) \ z) \ (y \ z)) by Th7
.= ((((x \ z) \ z) \ (z `)) \ y) \ (((x \ z) \ z) \ (y \ z)) by A2
.= ((((x \ z) \ z) \ (z `)) \ (((x \ z) \ z) \ (y \ z))) \ y by Th7
.= ((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y by Th7 ;
then ((x \ y) \ z) \ (((x \ z) \ z) \ (y \ z)) = 0. X by A4, Th2;
hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by A3, Def7; :: thesis: verum

end;

hence X is weakly-positive-implicative ; :: thesis: verum