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