let X be BCI-algebra; :: thesis: for K being closed Ideal of X
for RK being I-congruence of X,K holds Ker (nat_hom RK) = K
let K be closed Ideal of X; :: thesis: for RK being I-congruence of X,K holds Ker (nat_hom RK) = K
let RK be I-congruence of X,K; :: thesis: Ker (nat_hom RK) = K
set h = nat_hom RK;
set Y = X ./. RK;
thus Ker (nat_hom RK) c= K :: according to XBOOLE_0:def 10 :: thesis: K c= Ker (nat_hom RK)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Ker (nat_hom RK) or y in K )
assume y in Ker (nat_hom RK) ; :: thesis: y in K
then consider x being Element of X such that
D1: ( y = x & (nat_hom RK) . x = 0. (X ./. RK) ) ;
Class RK,(0. X) = Class RK,x by Def5, D1;
then x in Class RK,(0. X) by EQREL_1:31;
then [(0. X),x] in RK by EQREL_1:26;
then x \ (0. X) in K by BCIALG_2:def 12;
hence y in K by D1, BCIALG_1:2; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in K or y in Ker (nat_hom RK) )
assume D1: y in K ; :: thesis: y in Ker (nat_hom RK)
then reconsider x = y as Element of X ;
D3: x \ (0. X) in K by D1, BCIALG_1:2;
x ` in K by D1, BCIALG_1:def 19;
then [(0. X),x] in RK by D3, BCIALG_2:def 12;
then x in Class RK,(0. X) by EQREL_1:26;
then Class RK,(0. X) = Class RK,x by EQREL_1:31;
then (nat_hom RK) . x = 0. (X ./. RK) by Def5;
hence y in Ker (nat_hom RK) ; :: thesis: verum