:: deftheorem Def10 defines nat_hom BCIALG_6:def 10 :
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for b₄ being BCI-homomorphism of X,(X ./. RI) holds
( b₄ = nat_hom RI iff for x being Element of X holds b₄ . x = Class (RI,x) );