let X be BCI-algebra; :: thesis: for I being Ideal of X st I = BCK-part X holds
for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra
let I be Ideal of X; :: thesis: ( I = BCK-part X implies for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra )
assume A1: I = BCK-part X ; :: thesis: for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra
let RI be I-congruence of X,I; :: thesis: X ./. RI is p-Semisimple BCI-algebra
set IT = X ./. RI;
for w1 being Element of (X ./. RI) holds (w1 `) ` = w1

proof

let w1 be Element of (X ./. RI); :: thesis: (w1 `) ` = w1
w1 in the carrier of (X ./. RI) ;
then consider x1 being object such that
A2: x1 in the carrier of X and
A3: w1 = Class (RI,x1) by EQREL_1:def 3;
reconsider x1 = x1 as Element of X by A2;
w1 ` = Class (RI,(x1 `)) by A3, Def17;
then A4: (w1 `) ` = Class (RI,((x1 `) `)) by Def17;
x1 \ ((x1 `) `) is positive Element of X by Th28;
then 0. X <= x1 \ ((x1 `) `) by Def2;
then A5: x1 \ ((x1 `) `) in I by A1;
0. X in I by BCIALG_1:def 18;
then ((x1 `) `) \ x1 in I by BCIALG_1:1;
then [((x1 `) `),x1] in RI by A5, Def12;
hence (w1 `) ` = w1 by A3, A4, EQREL_1:35; :: thesis: verum

end;

hence X ./. RI is p-Semisimple BCI-algebra by BCIALG_1:54; :: thesis: verum