theorem Th84: :: BCIALG_1:84

for X being BCI-algebra holds
( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) )