let X be BCI-algebra; :: thesis: for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X
let x, y be Element of X; :: thesis: ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X
((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) \ (y \ x) by Th7
.= ((x \ (x \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (y \ x) by Th7
.= ((x \ (y \ (y \ x))) \ (x \ y)) \ (y \ x) by Th8
.= ((x \ (y \ (y \ x))) \ (x \ y)) \ (y \ (y \ (y \ x))) by Th8 ;
hence ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by Th1; :: thesis: verum