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