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

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, Def26;
hence z = x by Th2; :: thesis: verum

end;

hence x is atom by Def14; :: 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
A3: y is atom by A2;
(x \ (x \ y)) \ y = 0. X by Th1;
hence x \ (x \ y) = y by A3, Def14; :: thesis: verum

end;

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