let X be BCI-algebra; :: thesis: for x, a, b being Element of X st X is alternative & x \ a = x \ b holds

a = b

let x, a, b be Element of X; :: thesis: ( X is alternative & x \ a = x \ b implies a = b )

assume that

A1: X is alternative and

A2: x \ a = x \ b ; :: thesis: a = b

(x \ x) \ a = x \ (x \ b) by A1, A2;

then (x \ x) \ a = (x \ x) \ b by A1;

then a ` = (x \ x) \ b by Def5;

then a ` = b ` by Def5;

then a = b ` by A1, Th76;

hence a = b by A1, Th76; :: thesis: verum

a = b

let x, a, b be Element of X; :: thesis: ( X is alternative & x \ a = x \ b implies a = b )

assume that

A1: X is alternative and

A2: x \ a = x \ b ; :: thesis: a = b

(x \ x) \ a = x \ (x \ b) by A1, A2;

then (x \ x) \ a = (x \ x) \ b by A1;

then a ` = (x \ x) \ b by Def5;

then a ` = b ` by Def5;

then a = b ` by A1, Th76;

hence a = b by A1, Th76; :: thesis: verum