theorem Th3: :: BCIALG_1:3

for X being BCI-algebra
for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds
x \ z = 0. X