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