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

y = z )

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

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

y = z ) implies X is p-Semisimple )

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

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

for x being Element of X st x ` = 0. X holds

x = 0. X

y = z )

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

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

y = z ) implies X is p-Semisimple )

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

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

for x being Element of X st x ` = 0. X holds

x = 0. X

proof

hence
X is p-Semisimple
by Th62; :: thesis: verum
let x be Element of X; :: thesis: ( x ` = 0. X implies x = 0. X )

assume x ` = 0. X ; :: thesis: x = 0. X

then x ` = (0. X) ` by Def5;

hence x = 0. X by A1; :: thesis: verum

end;assume x ` = 0. X ; :: thesis: x = 0. X

then x ` = (0. X) ` by Def5;

hence x = 0. X by A1; :: thesis: verum