theorem :: BCIALG_1:78

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