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: z \ y = (z \ x) \ (y \ x) by A1, Lm11

.= 0. X by A2, Def5 ;

y \ z = (y \ x) \ (z \ x) by A1, Lm11

.= 0. X 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 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: z \ y = (z \ x) \ (y \ x) by A1, Lm11

.= 0. X by A2, Def5 ;

y \ z = (y \ x) \ (z \ x) by A1, Lm11

.= 0. X by A2, Def5 ;

hence y = z by A3, Def7; :: thesis: verum