K87() is set
K19(K87()) is set
K110() is set
K19(K110()) is set
K114() is Element of K19(K110())
{} is set
the empty set is empty set
1 is non empty set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
y \ I is Element of the carrier of X
y \ (y \ I) is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
I \ (x \ y) is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
I \ (x \ y) is Element of the carrier of X
(I \ (x \ y)) \ (I \ (x \ y)) is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (x \ y) is Element of the carrier of X
((I \ (x \ y)) \ (I \ (x \ y))) \ ((x \ y) \ (x \ y)) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
((I \ (x \ y)) \ (I \ (x \ y))) \ (y \ y) is Element of the carrier of X
((x \ y) \ (x \ y)) \ (y \ y) is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
((x \ y) \ (y \ y)) \ (x \ y) is Element of the carrier of X
(((I \ (x \ y)) \ (I \ (x \ y))) \ (y \ y)) \ (0. X) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ (y \ y) is Element of the carrier of X
I \ (x \ (y \ y)) is Element of the carrier of X
x is Element of the carrier of X
y \ x is Element of the carrier of X
x \ (y \ x) is Element of the carrier of X
I \ (x \ (y \ x)) is Element of the carrier of X
(I \ (x \ (y \ y))) \ (I \ (x \ (y \ x))) is Element of the carrier of X
x \ y is Element of the carrier of X
(x \ (y \ x)) \ (x \ (y \ y)) is Element of the carrier of X
((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ ((x \ (y \ x)) \ (x \ (y \ y))) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(y \ y) \ (y \ x) is Element of the carrier of X
((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ ((y \ y) \ (y \ x)) is Element of the carrier of X
((x \ (y \ x)) \ (x \ (y \ y))) \ ((y \ y) \ (y \ x)) is Element of the carrier of X
(x \ (y \ x)) \ ((y \ y) \ (y \ x)) is Element of the carrier of X
((x \ (y \ x)) \ ((y \ y) \ (y \ x))) \ (x \ (y \ y)) is Element of the carrier of X
(((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ ((y \ y) \ (y \ x))) \ (0. X) is Element of the carrier of X
((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ (x \ y) is Element of the carrier of X
((y \ y) \ (y \ x)) \ (x \ y) is Element of the carrier of X
(y \ y) \ (x \ y) is Element of the carrier of X
((y \ y) \ (x \ y)) \ (y \ x) is Element of the carrier of X
(((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ (x \ y)) \ (0. X) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
(0. X) \ (I \ x) is Element of the carrier of X
x \ I is Element of the carrier of X
((0. X) \ (I \ x)) \ (x \ I) is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
((0. X) \ I) \ ((0. X) \ x) is Element of the carrier of X
(((0. X) \ I) \ ((0. X) \ x)) \ (x \ I) is Element of the carrier of X
((0. X) \ I) \ (x \ I) is Element of the carrier of X
(((0. X) \ I) \ (x \ I)) \ ((0. X) \ x) is Element of the carrier of X
(x \ I) ` is Element of the carrier of X
(0. X) \ (x \ I) is Element of the carrier of X
((x \ I) `) \ I is Element of the carrier of X
(((x \ I) `) \ I) \ ((0. X) \ x) is Element of the carrier of X
x ` is Element of the carrier of X
I ` is Element of the carrier of X
(x `) \ (I `) is Element of the carrier of X
((x `) \ (I `)) \ I is Element of the carrier of X
(((x `) \ (I `)) \ I) \ ((0. X) \ x) is Element of the carrier of X
(x `) \ I is Element of the carrier of X
((x `) \ I) \ (I `) is Element of the carrier of X
(((x `) \ I) \ (I `)) \ ((0. X) \ x) is Element of the carrier of X
((x `) \ I) \ (x `) is Element of the carrier of X
(((x `) \ I) \ (x `)) \ (I `) is Element of the carrier of X
(x `) \ (x `) is Element of the carrier of X
((x `) \ (x `)) \ I is Element of the carrier of X
(((x `) \ (x `)) \ I) \ (I `) is Element of the carrier of X
(I `) \ (I `) is Element of the carrier of X
(I \ x) ` is Element of the carrier of X
((I \ x) `) \ (x \ I) is Element of the carrier of X
(I `) \ (x `) is Element of the carrier of X
((I `) \ (x `)) \ (x \ I) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : b1 <= I } is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of I
x \ y is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
AtomSet X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
{ b1 where b1 is Element of the carrier of X : b1 is atom } is set
x is Element of AtomSet X
y is Element of AtomSet X
BranchV y is non empty Element of K19( the carrier of X)
{ b1 where b1 is Element of the carrier of X : y <= b1 } is set
y is Element of AtomSet X
y \ x is Element of AtomSet X
y \ y is Element of AtomSet X
y \ x is Element of AtomSet X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
AtomSet X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
{ b1 where b1 is Element of the carrier of X : b1 is atom } is set
x is Element of the carrier of X
y is Element of AtomSet X
y is Element of AtomSet X
BranchV y is non empty Element of K19( the carrier of X)
{ b1 where b1 is Element of the carrier of X : y <= b1 } is set
x \ y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ y is Element of AtomSet X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of I
(X,x) is set
{ b1 where b1 is Element of the carrier of X : b1 <= x } is set
y is set
y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
AtomSet X is non empty Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is set
{ b1 where b1 is Element of the carrier of X : b1 is atom } is set
BCK-part X is non empty Element of K19( the carrier of X)
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
{(0. X)} is set
(BCK-part X) /\ (AtomSet X) is Element of K19( the carrier of X)
y is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
y is Element of BCK-part X
y is Element of AtomSet X
y \ y is Element of the carrier of X
y is Element of BCK-part X
y is Element of AtomSet X
y \ y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
AtomSet X is non empty Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is set
{ b1 where b1 is Element of the carrier of X : b1 is atom } is set
x is Element of AtomSet X
x ` is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(0. X) \ x is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{(0. X)} is set
I is non empty Ideal of X
x is non empty Ideal of X
I /\ x is Element of K19( the carrier of X)
K19( the carrier of X) is set
y is Element of I
y is Element of x
y \ y is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
(y \ (y \ y)) \ y is Element of the carrier of X
(y \ (y \ y)) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
(y \ y) \ (y \ y) is Element of the carrier of X
(y \ y) ` is Element of the carrier of X
(0. X) \ (y \ y) is Element of the carrier of X
(y \ y) \ y is Element of the carrier of X
(y \ y) \ y is Element of the carrier of X
y ` is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
y is set
y is Element of I
x is Element of x
y \ x is Element of the carrier of X
y is set
X is non empty being_B being_C being_I being_BCI-4 associative weakly-positive-implicative V67() alternative BCIStr_0
I is non empty Ideal of X
the carrier of X is non empty set
x is Element of I
x ` is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(0. X) \ x is Element of the carrier of X
x \ (0. X) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
I is non empty Ideal of X
the carrier of X is non empty set
x is Element of I
x ` is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(0. X) \ x is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is set
K19( the carrier of X) is set
x is non empty Ideal of X
y is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
K19( the carrier of X) is set
I is non empty Element of K19( the carrier of X)
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(x \ y) \ (0. X) is Element of the carrier of X
y \ (0. X) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ (y \ y) is Element of the carrier of X
x \ (x \ y) is Element of the carrier of X
(x \ (x \ y)) \ y is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(x \ (x \ y)) \ (y \ y) is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
((x \ (x \ y)) \ (y \ y)) \ y is Element of the carrier of X
(y \ (y \ y)) \ y is Element of the carrier of X
(((x \ (x \ y)) \ (y \ y)) \ y) \ (0. X) is Element of the carrier of X
(x \ (y \ y)) \ (x \ y) is Element of the carrier of X
((x \ (y \ y)) \ (x \ y)) \ y is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ (y \ y) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is non empty Ideal of X
x is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
x \ ((0. X) \ x) is Element of the carrier of X
x \ x is Element of the carrier of X
x \ (0. X) is Element of the carrier of X
(x \ (0. X)) \ x is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is non empty Ideal of X
x is Element of I
x ` is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
((0. X) \ x) \ x is Element of the carrier of X
(0. X) \ ((0. X) \ x) is Element of the carrier of X
(0. X) \ ((0. X) \ ((0. X) \ x)) is Element of the carrier of X
((0. X) \ ((0. X) \ ((0. X) \ x))) \ x is Element of the carrier of X
((0. X) \ x) \ ((0. X) \ ((0. X) \ x)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
K19( the carrier of X) is set
I is non empty Element of K19( the carrier of X)
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
x \ (0. X) is Element of the carrier of X
(x \ (0. X)) \ y is Element of the carrier of X
y \ (0. X) is Element of the carrier of X
(x \ (0. X)) \ (y \ (0. X)) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
BCK-part X is non empty Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
I is non empty Ideal of X
x is set
y is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
y is Element of the carrier of X
(0. X) \ ((0. X) \ y) is Element of the carrier of X
y \ y is Element of the carrier of X
(y \ y) \ ((0. X) \ y) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
BCK-part X is non empty Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
((x \ y) \ (y \ y)) ` is Element of the carrier of X
(0. X) \ ((x \ y) \ (y \ y)) is Element of the carrier of X
x is Element of the carrier of X
(x \ y) ` is Element of the carrier of X
(0. X) \ (x \ y) is Element of the carrier of X
(y \ y) ` is Element of the carrier of X
(0. X) \ (y \ y) is Element of the carrier of X
((x \ y) `) \ ((y \ y) `) is Element of the carrier of X
x ` is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
y ` is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
(x `) \ (y `) is Element of the carrier of X
((x `) \ (y `)) \ ((y \ y) `) is Element of the carrier of X
y ` is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
x is Element of the carrier of X
(0. X) \ (y `) is Element of the carrier of X
((x `) \ (y `)) \ ((0. X) \ (y `)) is Element of the carrier of X
(x `) \ (0. X) is Element of the carrier of X
(((x `) \ (y `)) \ ((0. X) \ (y `))) \ ((x `) \ (0. X)) is Element of the carrier of X
((x `) \ (0. X)) ` is Element of the carrier of X
(0. X) \ ((x `) \ (0. X)) is Element of the carrier of X
(x `) ` is Element of the carrier of X
(0. X) \ (x `) is Element of the carrier of X
(0. X) \ ((0. X) \ x) is Element of the carrier of X
(0. X) \ (0. X) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ x is Element of the carrier of X
(y \ x) ` is Element of the carrier of X
(0. X) \ (y \ x) is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
x \ y is Element of the carrier of X
((x \ y) \ (y \ y)) \ (x \ y) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
((x \ y) \ (y \ y)) \ (x \ y) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
x \ y is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
BCK-part X is non empty Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y ` is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) ` is Element of the carrier of X
(0. X) \ (x \ y) is Element of the carrier of X
y is Element of the carrier of X
x ` is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
(x `) \ (0. X) is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
x \ (y \ (y \ x)) is Element of the carrier of X
(0. X) \ (x \ (y \ (y \ x))) is Element of the carrier of X
(x \ (y \ (y \ x))) ` is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
BCK-part X is non empty Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
(x \ y) ` is Element of the carrier of X
(0. X) \ (x \ y) is Element of the carrier of X
y is Element of the carrier of X
x ` is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
y ` is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
(x `) \ (y `) is Element of the carrier of X
(x `) \ (0. X) is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
x \ (y \ (y \ x)) is Element of the carrier of X
(0. X) \ (x \ (y \ (y \ x))) is Element of the carrier of X
(x \ (y \ (y \ x))) ` is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
x is set
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
x is non empty Ideal of X
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
x is Element of the carrier of X
(y \ y) \ x is Element of the carrier of X
y \ y is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
y \ (y \ (y \ y)) is Element of the carrier of X
y \ (0. X) is Element of the carrier of X
y \ (y \ (0. X)) is Element of the carrier of X
y \ y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
I is set
x is Element of the carrier of X
x ` is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
BCK-part X is non empty Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
BCK-part X is non empty Element of K19( the carrier of X)
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
(x \ y) ` is Element of the carrier of X
(0. X) \ (x \ y) is Element of the carrier of X
y is Element of the carrier of X
x ` is Element of the carrier of X
(0. X) \ x is Element of the carrier of X
y ` is Element of the carrier of X
(0. X) \ y is Element of the carrier of X
(x `) \ (y `) is Element of the carrier of X
(x `) \ (0. X) is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
x \ (y \ (y \ x)) is Element of the carrier of X
(0. X) \ (x \ (y \ (y \ x))) is Element of the carrier of X
(x \ (y \ (y \ x))) ` is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
x \ (y \ (y \ x)) is Element of the carrier of X
(x \ y) \ (0. X) is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
x \ (y \ (y \ x)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
I is non empty Ideal of X
x is non empty Ideal of X
the carrier of X is non empty set
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
y \ y is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
y \ (y \ (y \ y)) is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
u is Element of the carrier of X
z is Element of the carrier of X
z \ x is Element of the carrier of X
u \ (z \ x) is Element of the carrier of X
z \ y is Element of the carrier of X
u \ (z \ y) is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
(y \ (y \ y)) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
(y \ y) \ (y \ y) is Element of the carrier of X
(y \ y) ` is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(0. X) \ (y \ y) is Element of the carrier of X
y \ (y \ (y \ y)) is Element of the carrier of X
y \ (y \ (y \ (y \ y))) is Element of the carrier of X
y \ (y \ (y \ (y \ (y \ y)))) is Element of the carrier of X
(y \ (y \ y)) \ y is Element of the carrier of X
(y \ y) \ (y \ y) is Element of the carrier of X
(y \ (y \ y)) \ (y \ (y \ (y \ (y \ y)))) is Element of the carrier of X
(y \ (y \ (y \ (y \ (y \ y))))) \ (y \ y) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is non empty Ideal of X
x is non empty Ideal of X
y is set
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I \ (x \ (x \ I)) is Element of the carrier of X
I \ (I \ x) is Element of the carrier of X
I \ (I \ (I \ x)) is Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I \ x is Element of the carrier of X
I \ (x \ (x \ I)) is Element of the carrier of X
(x \ (x \ I)) \ I is Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I \ (x \ (x \ I)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is non empty Ideal of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is non empty Ideal of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
x \ (x \ y) is Element of the carrier of X
(x \ y) \ x is Element of the carrier of X
(x \ y) \ ((x \ y) \ x) is Element of the carrier of X
x \ ((x \ y) \ ((x \ y) \ x)) is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
(y \ (y \ x)) \ x is Element of the carrier of X
(y \ (y \ x)) \ (x \ y) is Element of the carrier of X
x \ x is Element of the carrier of X
(x \ x) \ y is Element of the carrier of X
(x \ y) \ ((x \ x) \ y) is Element of the carrier of X
x \ ((x \ x) \ y) is Element of the carrier of X
(x \ ((x \ x) \ y)) \ y is Element of the carrier of X
y ` is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(0. X) \ y is Element of the carrier of X
x \ (y `) is Element of the carrier of X
(x \ (y `)) \ y is Element of the carrier of X
x \ (0. X) is Element of the carrier of X
(x \ (0. X)) \ y is Element of the carrier of X
y \ (0. X) is Element of the carrier of X
(y \ (0. X)) \ (y \ x) is Element of the carrier of X
((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) is Element of the carrier of X
(y \ (y \ x)) \ (x \ (0. X)) is Element of the carrier of X
((y \ (0. X)) \ (y \ x)) \ (x \ y) is Element of the carrier of X
(x \ (0. X)) \ (x \ y) is Element of the carrier of X
((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
I \ (I \ x) is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I \ (x \ (x \ I)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
I \ (I \ x) is Element of the carrier of X
x \ (I \ (I \ x)) is Element of the carrier of X
x \ (x \ (I \ (I \ x))) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is Element of the carrier of X
x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
0. X is V44(X) atom positive V87(X) Element of the carrier of X
the carrier of X is non empty set
{(0. X)} is set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
y \ y is Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
I is Element of the carrier of X
y \ I is Element of the carrier of X
y \ x is Element of the carrier of X
(y \ I) \ (y \ x) is Element of the carrier of X
x \ I is Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I \ (x \ (x \ I)) is Element of the carrier of X
I \ x is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
(y \ y) \ y is Element of the carrier of X
(y \ y) \ ((y \ y) \ y) is Element of the carrier of X
I is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
y \ x is Element of the carrier of X
y \ I is Element of the carrier of X
(y \ x) \ (y \ I) is Element of the carrier of X
(y \ x) \ ((y \ x) \ (y \ I)) is Element of the carrier of X
I \ x is Element of the carrier of X
(y \ x) \ (I \ x) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
I \ (I \ x) is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I is non empty Ideal of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I \ (x \ (x \ I)) is Element of the carrier of X
I is non empty Ideal of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
I \ (I \ x) is Element of the carrier of X
x \ (I \ (I \ x)) is Element of the carrier of X
x \ (x \ (I \ (I \ x))) is Element of the carrier of X
I is non empty Ideal of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I is non empty Ideal of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
y \ y is Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
I \ x is Element of the carrier of X
x \ I is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
I is Element of the carrier of X
y \ I is Element of the carrier of X
y \ x is Element of the carrier of X
(y \ I) \ (y \ x) is Element of the carrier of X
x \ I is Element of the carrier of X
I is Element of the carrier of X
x is Element of the carrier of X
x \ I is Element of the carrier of X
x \ (x \ I) is Element of the carrier of X
I \ (x \ (x \ I)) is Element of the carrier of X
I \ x is Element of the carrier of X
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
(y \ y) \ y is Element of the carrier of X
(y \ y) \ ((y \ y) \ y) is Element of the carrier of X
I is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
y \ x is Element of the carrier of X
y \ I is Element of the carrier of X
(y \ x) \ (y \ I) is Element of the carrier of X
(y \ x) \ ((y \ x) \ (y \ I)) is Element of the carrier of X
I \ x is Element of the carrier of X
(y \ x) \ (I \ x) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
y \ x is Element of the carrier of X
x \ (y \ x) is Element of the carrier of X
y is Element of the carrier of X
(x \ (y \ x)) \ y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
y \ x is Element of the carrier of X
x \ (y \ x) is Element of the carrier of X
y is Element of the carrier of X
(x \ (y \ x)) \ y is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
y \ x is Element of the carrier of X
x \ (y \ x) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(x \ (y \ x)) \ (0. X) is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
y \ x is Element of the carrier of X
x \ (y \ x) is Element of the carrier of X
y is Element of the carrier of X
x is Element of the carrier of X
x \ y is Element of the carrier of X
y \ (x \ y) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
K19( the carrier of X) is set
0. X is V44(X) atom positive V87(X) Element of the carrier of X
I is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
((x \ y) \ y) \ ((x \ y) \ y) is Element of the carrier of X
(x \ y) \ (x \ y) is Element of the carrier of X
(((x \ y) \ y) \ ((x \ y) \ y)) \ ((x \ y) \ (x \ y)) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(((x \ y) \ y) \ ((x \ y) \ y)) \ (y \ y) is Element of the carrier of X
((x \ y) \ (x \ y)) \ (y \ y) is Element of the carrier of X
((((x \ y) \ y) \ ((x \ y) \ y)) \ (y \ y)) \ (0. X) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
x \ (y \ y) is Element of the carrier of X
(x \ (y \ y)) \ (x \ y) is Element of the carrier of X
y \ (y \ y) is Element of the carrier of X
((x \ (y \ y)) \ (x \ y)) \ (y \ (y \ y)) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
((x \ (y \ y)) \ (x \ y)) \ y is Element of the carrier of X
(y \ (y \ y)) \ y is Element of the carrier of X
(y \ y) \ (y \ y) is Element of the carrier of X
(((x \ (y \ y)) \ (x \ y)) \ y) \ (0. X) is Element of the carrier of X
(x \ (y \ y)) \ y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ y is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
y \ y is Element of the carrier of X
x \ y is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ y is Element of the carrier of X
(x \ y) \ (y \ y) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
I is non empty Ideal of X
x is non empty Ideal of X
the carrier of X is non empty set
y is Element of the carrier of X
y is Element of the carrier of X
y \ y is Element of the carrier of X
(y \ y) \ y is Element of the carrier of X
y \ ((y \ y) \ y) is Element of the carrier of X
(y \ ((y \ y) \ y)) \ y is Element of the carrier of X
((y \ ((y \ y) \ y)) \ y) \ y is Element of the carrier of X
(y \ y) \ ((y \ y) \ y) is Element of the carrier of X
((y \ y) \ ((y \ y) \ y)) \ y is Element of the carrier of X
((y \ y) \ y) \ ((y \ y) \ y) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
I is non empty Ideal of X
the carrier of X is non empty set
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
y \ x is Element of the carrier of X
y \ (y \ x) is Element of the carrier of X
x \ (y \ (y \ x)) is Element of the carrier of X
(x \ (y \ (y \ x))) \ x is Element of the carrier of X
x \ x is Element of the carrier of X
(x \ x) \ (y \ (y \ x)) is Element of the carrier of X
(y \ (y \ x)) ` is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X
(0. X) \ (y \ (y \ x)) is Element of the carrier of X
y \ (x \ (y \ (y \ x))) is Element of the carrier of X
(x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) is Element of the carrier of X
(x \ (y \ (y \ x))) \ (y \ x) is Element of the carrier of X
((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) is Element of the carrier of X
((x \ (y \ (y \ x))) \ (y \ x)) \ (x \ y) is Element of the carrier of X
x \ (y \ x) is Element of the carrier of X
(x \ (y \ x)) \ (y \ (y \ x)) is Element of the carrier of X
(((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (0. X) is Element of the carrier of X
x is Element of the carrier of X
y is Element of the carrier of X
x \ y is Element of the carrier of X
(x \ y) \ y is Element of the carrier of X
x \ (x \ y) is Element of the carrier of X
(x \ y) \ (x \ (x \ y)) is Element of the carrier of X
((x \ y) \ (x \ (x \ y))) \ ((x \ y) \ y) is Element of the carrier of X
0. X is V44(X) atom positive V87(X) Element of the carrier of X