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