let X be BCI-algebra; :: thesis: for x, y being Element of X st X is alternative holds
( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )
let x, y be Element of X; :: thesis: ( X is alternative implies ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x ) )
assume A1: X is alternative ; :: thesis: ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x )
then x \ (x \ x) = (x \ x) \ x ;
then x \ (0. X) = (x \ x) \ x by Def5;
then x \ (0. X) = x ` by Def5;
hence x ` = x by Th2; :: thesis: ( x \ (x \ y) = y & (x \ y) \ y = x )
y \ (y \ y) = (y \ y) \ y by A1;
then y \ (0. X) = (y \ y) \ y by Def5;
then y \ (0. X) = y ` by Def5;
then A2: y = y ` by Th2;
x \ (x \ y) = (x \ x) \ y by A1;
hence x \ (x \ y) = y by A2, Def5; :: thesis: (x \ y) \ y = x
(x \ y) \ y = x \ (y \ y) by A1;
then (x \ y) \ y = x \ (0. X) by Def5;
hence (x \ y) \ y = x by Th2; :: thesis: verum