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 )
thus x ` = x :: thesis: ( x \ (x \ y) = y & (x \ y) \ y = x )

proof

x \ (x \ x) = (x \ x) \ x by A1, Def27;
then x \ (0. X) = (x \ x) \ x by Def5;
then x \ (0. X) = x ` by Def5;
hence x ` = x by Th2; :: thesis: verum

end;

thus x \ (x \ y) = y :: thesis: (x \ y) \ y = x

proof

y \ (y \ y) = (y \ y) \ y by A1, Def27;
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, Def27;
hence x \ (x \ y) = y by A2, Def5; :: thesis: verum

end;

(x \ y) \ y = x \ (y \ y) by A1, Def27;
then (x \ y) \ y = x \ (0. X) by Def5;
hence (x \ y) \ y = x by Th2; :: thesis: verum