let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds

y = z )

thus ( X is p-Semisimple implies for x, y, z being Element of X st y \ x = z \ x holds

y = z ) by Lm14; :: thesis: ( ( for x, y, z being Element of X st y \ x = z \ x holds

y = z ) implies X is p-Semisimple )

assume A1: for x, y, z being Element of X st y \ x = z \ x holds

y = z ; :: thesis: X is p-Semisimple

for x, y being Element of X holds x \ (x \ y) = y

y = z )

thus ( X is p-Semisimple implies for x, y, z being Element of X st y \ x = z \ x holds

y = z ) by Lm14; :: thesis: ( ( for x, y, z being Element of X st y \ x = z \ x holds

y = z ) implies X is p-Semisimple )

assume A1: for x, y, z being Element of X st y \ x = z \ x holds

y = z ; :: thesis: X is p-Semisimple

for x, y being Element of X holds x \ (x \ y) = y

proof

hence
X is p-Semisimple
; :: thesis: verum
let x, y be Element of X; :: thesis: x \ (x \ y) = y

(x \ (x \ y)) \ y = 0. X by Th1;

then (x \ (x \ y)) \ y = y \ y by Def5;

hence x \ (x \ y) = y by A1; :: thesis: verum

end;(x \ (x \ y)) \ y = 0. X by Th1;

then (x \ (x \ y)) \ y = y \ y by Def5;

hence x \ (x \ y) = y by A1; :: thesis: verum