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

x \ z = 0. X

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

assume that

A1: x \ y = 0. X and

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

((x \ z) \ (x \ y)) \ (y \ z) = 0. X by Th1;

then (x \ z) \ (x \ y) = 0. X by A2, Th2;

hence x \ z = 0. X by A1, Th2; :: thesis: verum

x \ z = 0. X

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

assume that

A1: x \ y = 0. X and

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

((x \ z) \ (x \ y)) \ (y \ z) = 0. X by Th1;

then (x \ z) \ (x \ y) = 0. X by A2, Th2;

hence x \ z = 0. X by A1, Th2; :: thesis: verum