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