theorem :: BCIALG_1:77

for X being BCI-algebra
for x, a, b being Element of X st X is alternative & x \ a = x \ b holds
a = b