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 set such that
A2: x1 in the carrier of X and
A3: w1 = Class RI,x1 by EQREL_1:def 5;
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:44; :: thesis: verum

end;

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