theorem :: BCIALG_1:79

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