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

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