let X be BCI-algebra; :: thesis: ( X is alternative implies X is implicative )
assume X is alternative ; :: thesis: X is implicative
then for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by Th76;
hence X is implicative by Def24; :: thesis: verum