let X be BCI-algebra; :: thesis: for x, y being Element of X st X is weakly-positive-implicative holds
(x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)
let x, y be Element of X; :: thesis: ( X is weakly-positive-implicative implies (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) )
assume A1: X is weakly-positive-implicative ; :: thesis: (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)
((x \ (x \ y)) \ (y \ (x \ y))) \ (x \ y) = 0. X by Def3;
then ((x \ (x \ y)) \ (x \ y)) \ (y \ (x \ y)) = 0. X by Th7;
then (((x \ (x \ y)) \ (x \ y)) \ ((x \ y) `)) \ ((y \ (x \ y)) \ ((x \ y) `)) = 0. X by Th4;
then ((((x \ (x \ y)) \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) \ (((y \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) = 0. X by Th4;
then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) = 0. X by A1, Th84;
then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (((x \ y) `) \ (y \ x))) = 0. X by A1;
then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (((x \ x) \ (x \ y)) \ (y \ x))) = 0. X by Def5;
then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (0. X)) = 0. X by Th1;
then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (x \ y)) \ (y \ x)) \ (y \ x)) = 0. X by Th2;
then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (y \ x)) \ (x \ y)) \ (y \ x)) = 0. X by Th7;
then A2: ((x \ (x \ y)) \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) = 0. X by Th7;
((y \ (y \ x)) \ (y \ x)) \ (x \ (y \ x)) = 0. X by Th1;
then (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) \ ((x \ (y \ x)) \ (x \ y)) = 0. X by Th4;
then (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by Th7;
hence (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by A2, Def7; :: thesis: verum