begin
Lm1:
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff for x being Element of X st x <= a holds
x = a )
Lm2:
for X being BCI-algebra holds 0. X is positive
Lm3:
for X being BCI-algebra holds 0. X is minimal
begin
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
Element of
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
definition
let X be
BCI-algebra;
let E be
Congruence of
X;
existence
ex b1 being BinOp of (Class E) st
for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y))
uniqueness
for b1, b2 being BinOp of (Class E) st ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y)) ) & ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b2 . (W1,W2) = Class (E,(x \ y)) ) holds
b1 = b2
end;
:: n=0: it=x; n=1:it =x*y; n=2:it=(x*y)*y...