begin
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
begin
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
begin
Lm8:
for X being BCI-algebra holds
( ( for x being Element of X holds (x `) ` = x ) iff for x, y being Element of X holds y \ (y \ x) = x )
Lm9:
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 )
Lm10:
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) )
Lm11:
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
Lm12:
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
Lm13:
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
Lm14:
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 `)
Lm15:
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
begin
Lm16:
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) `
Lm17:
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) `
Lm18:
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
Lm19:
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
Lm20:
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) )
begin
Lm21:
for X being BCI-algebra holds
( X is alternative iff X is associative )
Lm22:
for X being BCI-algebra st X is alternative holds
X is implicative
begin
Lm23:
for X being BCI-algebra st X is associative holds
X is weakly-positive-implicative
Lm24:
for X being BCI-algebra st X is p-Semisimple BCI-algebra holds
X is weakly-positive-implicative BCI-algebra
Lm25:
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)
Lm26:
for X being BCI-algebra holds
( X is positive-implicative iff X is weakly-positive-implicative )