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