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

x = y

let x, y be Element of X; :: thesis: ( X is alternative & x \ y = 0. X implies x = y )

assume that

A1: X is alternative and

A2: x \ y = 0. X ; :: thesis: x = y

x \ (x \ y) = x by A2, Th2;

then (x \ x) \ y = x by A1;

then y ` = x by Def5;

hence x = y by A1, Th76; :: thesis: verum

x = y

let x, y be Element of X; :: thesis: ( X is alternative & x \ y = 0. X implies x = y )

assume that

A1: X is alternative and

A2: x \ y = 0. X ; :: thesis: x = y

x \ (x \ y) = x by A2, Th2;

then (x \ x) \ y = x by A1;

then y ` = x by Def5;

hence x = y by A1, Th76; :: thesis: verum