let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x being Element of X holds x is atom )
thus ( X is p-Semisimple implies for x being Element of X holds x is atom ) :: thesis: ( ( for x being Element of X holds x is atom ) implies X is p-Semisimple )

proof

assume A1: X is p-Semisimple ; :: thesis: for x being Element of X holds x is atom
let x be Element of X; :: thesis: x is atom

now :: thesis: for z being Element of X st z \ x = 0. X holds
z = x

let z be Element of X; :: thesis: ( z \ x = 0. X implies z = x )
assume z \ x = 0. X ; :: thesis: z = x
then z \ (0. X) = x by A1;
hence z = x by Th2; :: thesis: verum

end;

hence x is atom ; :: thesis: verum

end;

assume A2: for x being Element of X holds x is atom ; :: thesis: X is p-Semisimple
for x, y being Element of X holds x \ (x \ y) = y

proof

let x, y be Element of X; :: thesis: x \ (x \ y) = y
( y is atom & (x \ (x \ y)) \ y = 0. X ) by A2, Th1;
hence x \ (x \ y) = y ; :: thesis: verum

end;

hence X is p-Semisimple ; :: thesis: verum