let X be BCI-algebra; :: thesis: ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) )
assume A1: X is p-Semisimple ; :: thesis: for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `)
let x, y, z be Element of X; :: thesis: x \ (y \ z) = (z \ y) \ (x `)
x \ (y \ z) = z \ (y \ x) by A1, Th57
.= (z \ (0. X)) \ (y \ x) by Th2 ;
hence x \ (y \ z) = (z \ y) \ (x `) by A1, Lm9; :: thesis: verum