theorem
for
X being
BCI-algebra st ( for
X being
BCI-algebra for
x,
y being
Element of
X ex
i,
j,
m,
n being
Nat st (
((x,(x \ y)) to_power i),
(y \ x))
to_power j = (
((y,(y \ x)) to_power m),
(x \ y))
to_power n ) holds
for
E being
Congruence of
X for
I being
Ideal of
X st
I = Class (
E,
(0. X)) holds
E is
I-congruence of
X,
I