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 )

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

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 A2:
for x being Element of X holds x is atom
; :: thesis: X is p-Semisimple
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

end;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

hence
x is atom
; :: thesis: verumz = 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;assume z \ x = 0. X ; :: thesis: z = x

then z \ (0. X) = x by A1;

hence z = x by Th2; :: thesis: verum

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

( y is atom & (x \ (x \ y)) \ y = 0. X ) by A2, Th1;

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

end;( y is atom & (x \ (x \ y)) \ y = 0. X ) by A2, Th1;

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