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 object ; :: 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
A1: y = x and
A2: (nat_hom RK) . x = 0. (X ./. RK) ;
Class (RK,(0. X)) = Class (RK,x) by A2, Def10;
then x in Class (RK,(0. X)) by EQREL_1:23;
then [(0. X),x] in RK by EQREL_1:18;
then x \ (0. X) in K by BCIALG_2:def 12;
hence y in K by A1, BCIALG_1:2; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in K or y in Ker (nat_hom RK) )
assume A3: y in K ; :: thesis: y in Ker (nat_hom RK)
then reconsider x = y as Element of X ;
( x \ (0. X) in K & x ` in K ) by A3, BCIALG_1:2, BCIALG_1:def 19;
then [(0. X),x] in RK by BCIALG_2:def 12;
then x in Class (RK,(0. X)) by EQREL_1:18;
then Class (RK,(0. X)) = Class (RK,x) by EQREL_1:23;
then (nat_hom RK) . x = 0. (X ./. RK) by Def10;
hence y in Ker (nat_hom RK) ; :: thesis: verum