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

( 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