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

(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