theorem :: BCIIDEAL:4

for X being BCI-algebra
for x, y being Element of X holds ((0. X) \ (x \ y)) \ (y \ x) = 0. X