let X be BCI-algebra; for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra
let G be SubAlgebra of X; for K being closed Ideal of X
for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra
let K be closed Ideal of X; for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra
let RK be I-congruence of X,K; HK (G,RK) is BCI-algebra
reconsider IT = HK (G,RK) as non empty BCIStr_0 ;
A1:
IT is being_BCI-4
A4:
IT is being_C
IT is being_I
hence
HK (G,RK) is BCI-algebra
by A2, A4, A1, BCIALG_1:def 3; verum