environ
vocabularies HIDDEN, BCIALG_1, CARD_FIL, SUBSET_1, FUNCT_1, NUMBERS, STRUCT_0, POWER, CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, FUNCOP_1, NAT_1, SUPINF_2, RELAT_1, CHORD, WAYBEL15, GROUP_4, GROUP_1, ALG_1, EQREL_1, PARTFUN1, RELAT_2, ZFMISC_1, RCOMP_1, TARSKI, BINOP_1, GROUP_6, BCIALG_2, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, FUNCT_2, XXREAL_0, FUNCOP_1, BINOP_1, STRUCT_0, BCIALG_1, RELAT_2, PARTFUN1, EQREL_1, ALG_1;
definitions XBOOLE_0, TARSKI, RELAT_1;
theorems BCIALG_1, FUNCOP_1, NAT_1, XREAL_1, TARSKI, XBOOLE_0, RELAT_2, RELAT_1, XXREAL_0, ORDERS_1, XBOOLE_1, BINOP_1, EQREL_1, RELSET_1, ZFMISC_1, ORDINAL1;
schemes FUNCT_2, NAT_1, RELSET_1, XBOOLE_0, BINOP_1;
registrations BCIALG_1, SUBSET_1, NAT_1, RELSET_1, STRUCT_0, PARTFUN1, ORDINAL1, XREAL_0, CARD_1;
constructors HIDDEN, BCIALG_1, BINOP_1, NAT_1, BINARITH, EQREL_1, RELSET_1, XREAL_0, NUMBERS, FUNCOP_1;
requirements HIDDEN, NUMERALS, ARITHM, SUBSET, BOOLE;
equalities STRUCT_0, BCIALG_1, RELAT_1;
expansions BCIALG_1;
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 )
by BCIALG_1:def 11;
Lm2:
for X being BCI-algebra holds 0. X is positive
Lm3:
for X being BCI-algebra holds 0. X is minimal
by BCIALG_1:2;
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
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...