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