let X be BCI-algebra; :: thesis: for x, a, b being Element of X st X is alternative & a \ x = b \ x holds
a = b
let x, a, b be Element of X; :: thesis: ( X is alternative & a \ x = b \ x implies a = b )
assume that
A1: X is alternative and
A2: a \ x = b \ x ; :: thesis: a = b
a \ (x \ x) = (b \ x) \ x by A1, A2;
then a \ (x \ x) = b \ (x \ x) by A1;
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