theorem :: BCIALG_1:85

for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds
for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by Lm24;