let X be BCI-algebra; :: thesis: ( X is positive-implicative iff X is weakly-positive-implicative )
thus ( X is positive-implicative implies X is weakly-positive-implicative ) :: thesis: ( X is weakly-positive-implicative implies X is positive-implicative )

proof

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

proof

let x, y be Element of X; :: thesis: x \ y = ((x \ y) \ y) \ (y `)
((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) by A1;
then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ (x \ y)) by Th8;
then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (0. X) by Def5;
then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = x \ y by Th2;
then ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) = x \ y by Th7;
then ((x \ y) \ (x \ (x \ y))) \ ((x \ x) \ y) = x \ y by Th7;
then ((x \ (x \ (x \ y))) \ y) \ ((x \ x) \ y) = x \ y by Th7;
then ((x \ y) \ y) \ ((x \ x) \ y) = x \ y by Th8;
hence x \ y = ((x \ y) \ y) \ (y `) by Def5; :: thesis: verum

end;

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

end;

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

proof

let x, y be Element of X; :: thesis: (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x)))
A3: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) by A2, Lm24;
(y \ (y \ x)) \ x = 0. X by Th1;
then (x \ x) \ (x \ (y \ (y \ x))) = 0. X by Th4;
then (x \ (y \ (y \ x))) ` = 0. X by Def5;
then x \ (x \ (y \ (y \ x))) = ((x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x)))) \ (0. X) by A2, Th84;
then x \ (x \ (y \ (y \ x))) = (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) by Th2;
then (x \ (x \ (y \ (y \ x)))) \ ((y \ (y \ x)) \ (x \ (y \ (y \ x)))) = 0. X by Th1;
then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((y \ (y \ x)) \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) = 0. X by Th4;
then A4: ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (x \ (y \ (y \ x)))) = 0. X by Th7;
((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) `)) = ((((y \ (y \ x)) \ (y \ x)) \ ((y \ x) `)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) `)) by A2, Th84
.= 0. X by Th1 ;
then (((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (x \ (y \ (y \ x)))) \ (((x \ y) \ ((y \ x) `)) \ (x \ (y \ (y \ x)))) = 0. X by Th4;
then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((x \ y) \ ((y \ x) `)) \ (x \ (y \ (y \ x)))) = 0. X by A4, Th3;
then A5: ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ x) `)) = 0. X by Th7;
((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ (y \ x)) \ y) = 0. X by Th1;
then ((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ y) \ (y \ x)) = 0. X by Th7;
then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (0. X) = 0. X by A5, Def5;
then A6: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by A3, Th2;
((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by Th10;
hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A6, Def7; :: thesis: verum

end;

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