let X be BCI-algebra; ( 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
; for x, y, z being Element of X st y \ x = z \ x holds
y = z
let x, y, z be Element of X; ( y \ x = z \ x implies y = z )
assume A2:
y \ x = z \ x
; 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; verum