environ
vocabularies HIDDEN, STRUCT_0, BINOP_1, XBOOLE_0, SUBSET_1, FUNCT_1, SUPINF_2, FUNCT_5, ZFMISC_1, UNIALG_2, TARSKI, REALSET1, RELAT_1, XXREAL_0, WAYBEL15, CARD_FIL, RCOMP_1, FILTER_0, BCIALG_1, CARD_1;
notations HIDDEN, TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, ORDINAL1, BINOP_1, FUNCT_5, REALSET1, STRUCT_0, RELAT_1;
definitions TARSKI, XBOOLE_0, STRUCT_0;
theorems TARSKI, ZFMISC_1, XBOOLE_0, STRUCT_0, FUNCT_2;
schemes ;
registrations RELAT_1, STRUCT_0, CARD_1;
constructors HIDDEN, BINOP_1, REALSET1, MIDSP_1, FUNCT_5, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities REALSET1, XBOOLE_0, ORDINAL1;
expansions STRUCT_0;
Lm1:
for X being BCI-algebra
for x being Element of X st x \ (0. X) = 0. X holds
x = 0. X
Lm2:
for X being BCI-algebra
for a being Element of AtomSet X
for x being Element of BranchV a holds a \ x = 0. X
Lm3:
for X being BCI-algebra holds {(0. X)} is Ideal of X
Lm4:
for X being BCI-algebra
for X1 being Ideal of X st X1 = {(0. X)} holds
for x being Element of X1 holds x ` in {(0. X)}
Lm5:
for X being BCI-algebra
for IT being non empty Subset of X st IT is Ideal of X holds
for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT
Lm6:
for X being BCI-algebra st ( for x, y being Element of X holds y \ x = x \ y ) holds
X is associative
Lm7:
for X being BCI-algebra st ( for x being Element of X holds x ` = x ) holds
for x, y being Element of X holds x \ y = y \ x
Lm8:
for X being BCI-algebra holds
( ( for x, y being Element of X holds y \ (y \ x) = x ) iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )
Lm9:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z, u being Element of X holds
( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) )
Lm10:
for X being BCI-algebra st X is p-Semisimple holds
for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y
Lm11:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z
Lm12:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st x \ y = x \ z holds
y = z
Lm13:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `)
Lm14:
for X being BCI-algebra st X is p-Semisimple holds
for x, y, z being Element of X st y \ x = z \ x holds
y = z
Lm15:
for X being BCI-algebra st ( for x being Element of X holds x ` <= x ) holds
for x, y being Element of X holds (x \ y) ` = (y \ x) `
Lm16:
for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) holds
for x, y being Element of X holds (x `) \ y = (x \ y) `
Lm17:
for X being BCI-algebra st ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) holds
for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X
Lm18:
for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) holds
X is quasi-associative
Lm19:
for X being BCI-algebra holds
( ( for x being Element of X holds x ` <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) )
Lm20:
for X being BCI-algebra holds
( X is alternative iff X is associative )
Lm21:
for X being BCI-algebra st X is alternative holds
X is implicative
by Th76;
Lm22:
for X being BCI-algebra st X is associative holds
X is weakly-positive-implicative
Lm23:
for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is weakly-positive-implicative BCI-algebra
Lm24:
for X being BCI-algebra
for x, y being Element of X st X is weakly-positive-implicative holds
(x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y)
Lm25:
for X being BCI-algebra holds
( X is positive-implicative iff X is weakly-positive-implicative )