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