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

( 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