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

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