theorem Th10: :: BCIALG_1:10

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