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