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

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