:: BCIALG_3 semantic presentation

K87() is set
K19(K87()) is set
{} is set
1 is set
BCI-EXAMPLE is non empty V42() V43() V48(1) strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative V67() weakly-implicative p-Semisimple alternative BCIStr_0
the U1 of BCI-EXAMPLE is non empty V12() V28() set
X is Element of the U1 of BCI-EXAMPLE
a is Element of the U1 of BCI-EXAMPLE
X \ a is Element of the U1 of BCI-EXAMPLE
X \ (X \ a) is Element of the U1 of BCI-EXAMPLE
a \ X is Element of the U1 of BCI-EXAMPLE
a \ (a \ X) is Element of the U1 of BCI-EXAMPLE
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(a \ (a \ x)) \ (x \ (x \ a)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (a \ (a \ x)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(a \ (a \ x)) \ (x \ (x \ a)) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
(a \ (a \ x)) \ ((0. X) \ (a \ x)) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
((a \ (a \ x)) \ ((0. X) \ (a \ x))) \ (a \ (0. X)) is Element of the U1 of X
(a \ (a \ x)) \ (0. X) is Element of the U1 of X
((a \ (a \ x)) \ (0. X)) \ a is Element of the U1 of X
(a \ (a \ x)) \ x is Element of the U1 of X
(a \ (a \ x)) \ a is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a \ (a \ (x \ (x \ a))) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ x is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(a \ (a \ x)) \ a is Element of the U1 of X
a \ a is Element of the U1 of X
(a \ a) \ (a \ x) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ x)) \ x is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
X is non empty BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
a \ ((0. X) \ x) is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ y) \ (a \ x) is Element of the U1 of X
x \ y is Element of the U1 of X
x \ a is Element of the U1 of X
(x \ y) \ (x \ a) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ y is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ y is Element of the U1 of X
x ` is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
a \ ((0. X) \ x) is Element of the U1 of X
(a \ ((0. X) \ x)) \ (a \ x) is Element of the U1 of X
x \ ((0. X) \ x) is Element of the U1 of X
(x \ ((0. X) \ x)) \ (x \ a) is Element of the U1 of X
a is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(0. X) \ (0. X) is Element of the U1 of X
(0. X) \ ((0. X) \ (0. X)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (0. X) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
(x \ (0. X)) \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
a \ a is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(0. X) \ (0. X) is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
((0. X) \ (0. X)) \ ((0. X) \ a) is Element of the U1 of X
(0. X) \ ((0. X) \ a) is Element of the U1 of X
a is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
((0. X) \ a) \ ((0. X) \ a) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
(a \ x) \ (a \ y) is Element of the U1 of X
y \ x is Element of the U1 of X
((a \ x) \ (a \ y)) \ (y \ x) is Element of the U1 of X
y \ a is Element of the U1 of X
(y \ x) \ (y \ a) is Element of the U1 of X
((y \ x) \ (y \ a)) \ (y \ x) is Element of the U1 of X
(y \ x) \ (0. X) is Element of the U1 of X
((y \ x) \ (y \ a)) \ ((y \ x) \ (0. X)) is Element of the U1 of X
(0. X) \ (y \ a) is Element of the U1 of X
(0. X) \ (y \ x) is Element of the U1 of X
((0. X) \ (y \ a)) \ ((0. X) \ (y \ x)) is Element of the U1 of X
(0. X) \ ((0. X) \ (y \ x)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ x is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (a \ x) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
((a \ (0. X)) \ (a \ x)) \ (x \ (0. X)) is Element of the U1 of X
(a \ (a \ x)) \ (x \ (0. X)) is Element of the U1 of X
a is Element of the U1 of X
a ` is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ a is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ (0. X) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
x is Element of the U1 of X
y is Element of the U1 of X
a is Element of the U1 of X
y \ a is Element of the U1 of X
y \ x is Element of the U1 of X
(y \ a) \ (y \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ y is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
y \ (y \ x) is Element of the U1 of X
(y \ (y \ x)) \ a is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
(x \ (0. X)) \ a is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
x is Element of the U1 of X
a is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ a is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
z is Element of the U1 of X
y is Element of the U1 of X
z \ y is Element of the U1 of X
z \ (z \ y) is Element of the U1 of X
y \ z is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ a is Element of the U1 of X
(a \ x) \ ((a \ x) \ a) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
y is Element of the U1 of X
x is Element of the U1 of X
y \ x is Element of the U1 of X
y \ a is Element of the U1 of X
(y \ x) \ (y \ a) is Element of the U1 of X
(y \ x) \ ((y \ x) \ (y \ a)) is Element of the U1 of X
a \ x is Element of the U1 of X
(y \ x) \ (a \ x) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
the U1 of BCI-EXAMPLE is non empty V12() V28() set
a is Element of the U1 of BCI-EXAMPLE
x is Element of the U1 of BCI-EXAMPLE
a \ x is Element of the U1 of BCI-EXAMPLE
0. BCI-EXAMPLE is V44( BCI-EXAMPLE ) Element of the U1 of BCI-EXAMPLE
x \ a is Element of the U1 of BCI-EXAMPLE
x \ (x \ a) is Element of the U1 of BCI-EXAMPLE
the U1 of BCI-EXAMPLE is non empty V12() V28() set
a is Element of the U1 of BCI-EXAMPLE
x is Element of the U1 of BCI-EXAMPLE
a \ x is Element of the U1 of BCI-EXAMPLE
a \ (a \ x) is Element of the U1 of BCI-EXAMPLE
0. BCI-EXAMPLE is V44( BCI-EXAMPLE ) Element of the U1 of BCI-EXAMPLE
(0. BCI-EXAMPLE) \ (a \ x) is Element of the U1 of BCI-EXAMPLE
(a \ (a \ x)) \ ((0. BCI-EXAMPLE) \ (a \ x)) is Element of the U1 of BCI-EXAMPLE
x \ a is Element of the U1 of BCI-EXAMPLE
x \ (x \ a) is Element of the U1 of BCI-EXAMPLE
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x is Element of the U1 of X
x ` is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ a is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ ((0. X) \ (a \ x)) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(0. X) \ (0. X) is Element of the U1 of X
((0. X) \ (0. X)) \ (a \ x) is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
((0. X) \ a) \ ((0. X) \ x) is Element of the U1 of X
(x \ a) \ ((0. X) \ (0. X)) is Element of the U1 of X
(x \ a) \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ ((0. X) \ (a \ x)) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(0. X) \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ ((0. X) \ (0. X)) is Element of the U1 of X
(a \ (0. X)) \ (0. X) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
(a \ (a \ x)) \ x is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
y is Element of the U1 of X
z is Element of the U1 of X
y \ z is Element of the U1 of X
y \ (y \ z) is Element of the U1 of X
z \ (y \ (y \ z)) is Element of the U1 of X
z \ (z \ (y \ (y \ z))) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ a is Element of the U1 of X
(x \ a) \ (x \ a) is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (x \ (x \ a)) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(a \ (a \ x)) \ (x \ (x \ a)) is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
(x \ (x \ (a \ (a \ x)))) \ (x \ (x \ a)) is Element of the U1 of X
x \ (x \ (x \ a)) is Element of the U1 of X
(x \ (x \ (x \ a))) \ (x \ (a \ (a \ x))) is Element of the U1 of X
(x \ a) \ (x \ (a \ (a \ x))) is Element of the U1 of X
(x \ (x \ (a \ (a \ x)))) \ a is Element of the U1 of X
(a \ (a \ x)) \ a is Element of the U1 of X
a \ a is Element of the U1 of X
(a \ a) \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(a \ (a \ x)) \ (x \ (x \ a)) is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
y is Element of the U1 of X
z is Element of the U1 of X
y \ z is Element of the U1 of X
y \ (y \ z) is Element of the U1 of X
z \ y is Element of the U1 of X
z \ (z \ y) is Element of the U1 of X
(y \ (y \ z)) \ (z \ (z \ y)) is Element of the U1 of X
(0. X) \ (y \ z) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
AtomSet X is non empty Element of K19( the U1 of X)
K19( the U1 of X) is set
{ b₁ where b₁ is Element of the U1 of X : b₁ is V60(X) } is set
a is Element of AtomSet X
BranchV a is non empty Element of K19( the U1 of X)
{ b₁ where b₁ is Element of the U1 of X : a <= b₁ } is set
x is Element of BranchV a
y is Element of BranchV a
x \ y is Element of the U1 of X
x \ (x \ y) is Element of the U1 of X
y \ x is Element of the U1 of X
y \ (y \ x) is Element of the U1 of X
a \ a is Element of AtomSet X
BranchV (a \ a) is non empty Element of K19( the U1 of X)
{ b₁ where b₁ is Element of the U1 of X : a \ a <= b₁ } is set
0. X is V44(X) Element of the U1 of X
z is Element of the U1 of X
(0. X) \ (y \ x) is Element of the U1 of X
(y \ (y \ x)) \ (x \ (x \ y)) is Element of the U1 of X
z is Element of the U1 of X
(0. X) \ (x \ y) is Element of the U1 of X
(x \ (x \ y)) \ (y \ (y \ x)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
(0. X) \ ((0. X) \ a) is Element of the U1 of X
((0. X) \ ((0. X) \ a)) ` is Element of the U1 of X
(0. X) \ ((0. X) \ ((0. X) \ a)) is Element of the U1 of X
(((0. X) \ ((0. X) \ a)) `) ` is Element of the U1 of X
(0. X) \ (((0. X) \ ((0. X) \ a)) `) is Element of the U1 of X
((0. X) \ ((0. X) \ a)) \ a is Element of the U1 of X
((0. X) \ a) \ ((0. X) \ a) is Element of the U1 of X
((0. X) \ ((0. X) \ a)) \ x is Element of the U1 of X
z is Element of AtomSet X
BranchV z is non empty Element of K19( the U1 of X)
{ b₁ where b₁ is Element of the U1 of X : z <= b₁ } is set
a \ (a \ x) is Element of the U1 of X
X is non empty BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
(a \ x) \ (a \ y) is Element of the U1 of X
y \ x is Element of the U1 of X
((a \ x) \ (a \ y)) \ (y \ x) is Element of the U1 of X
z is Element of the U1 of X
z \ (0. X) is Element of the U1 of X
c₆ is Element of the U1 of X
c₇ is Element of the U1 of X
c₆ \ c₇ is Element of the U1 of X
c₆ \ (c₆ \ c₇) is Element of the U1 of X
c₇ \ (c₆ \ (c₆ \ c₇)) is Element of the U1 of X
c₇ \ (c₇ \ (c₆ \ (c₆ \ c₇))) is Element of the U1 of X
c₈ is Element of the U1 of X
c₉ is Element of the U1 of X
c₈ \ c₉ is Element of the U1 of X
c₁₀ is Element of the U1 of X
c₈ \ c₁₀ is Element of the U1 of X
(c₈ \ c₉) \ (c₈ \ c₁₀) is Element of the U1 of X
c₁₀ \ c₉ is Element of the U1 of X
((c₈ \ c₉) \ (c₈ \ c₁₀)) \ (c₁₀ \ c₉) is Element of the U1 of X
c₁₁ is Element of the U1 of X
c₁₁ \ (0. X) is Element of the U1 of X
c₁₂ is Element of the U1 of X
c₁₃ is Element of the U1 of X
c₁₂ \ c₁₃ is Element of the U1 of X
c₁₂ \ (c₁₂ \ c₁₃) is Element of the U1 of X
c₁₃ \ (c₁₂ \ (c₁₂ \ c₁₃)) is Element of the U1 of X
c₁₃ \ (c₁₃ \ (c₁₂ \ (c₁₂ \ c₁₃))) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
x \ (x \ (x \ a)) is Element of the U1 of X
(x \ (x \ (x \ a))) \ (x \ a) is Element of the U1 of X
(x \ a) \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
(x \ (x \ a)) \ a is Element of the U1 of X
a is Element of the U1 of X
y is Element of the U1 of X
x is Element of the U1 of X
y \ x is Element of the U1 of X
y \ a is Element of the U1 of X
a \ y is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
y \ (y \ a) is Element of the U1 of X
(y \ x) \ (y \ a) is Element of the U1 of X
a \ x is Element of the U1 of X
a is Element of the U1 of X
y is Element of the U1 of X
x is Element of the U1 of X
y \ x is Element of the U1 of X
y \ a is Element of the U1 of X
a is Element of the U1 of X
y is Element of the U1 of X
x is Element of the U1 of X
y \ x is Element of the U1 of X
y \ a is Element of the U1 of X
z is Element of the U1 of X
c₇ is Element of the U1 of X
c₆ is Element of the U1 of X
c₇ \ c₆ is Element of the U1 of X
c₇ \ z is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
x \ (x \ y) is Element of the U1 of X
a \ y is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ y)) is Element of the U1 of X
x \ (x \ (x \ y)) is Element of the U1 of X
(x \ (x \ (x \ y))) \ (x \ a) is Element of the U1 of X
(x \ y) \ (x \ a) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
x \ (x \ y) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ a is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
(x \ (x \ a)) \ a is Element of the U1 of X
(x \ a) \ (x \ a) is Element of the U1 of X
the U1 of BCI-EXAMPLE is non empty V12() V28() set
the Element of the U1 of BCI-EXAMPLE is Element of the U1 of BCI-EXAMPLE
0. BCI-EXAMPLE is V44( BCI-EXAMPLE ) Element of the U1 of BCI-EXAMPLE
x is Element of the U1 of BCI-EXAMPLE
x \ the Element of the U1 of BCI-EXAMPLE is Element of the U1 of BCI-EXAMPLE
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
a \ y is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ y) \ (a \ x) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ y is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
a \ y is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ y) \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(a \ (a \ x)) \ (0. X) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (a \ x) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
x \ (a \ y) is Element of the U1 of X
a \ x is Element of the U1 of X
y \ (a \ x) is Element of the U1 of X
a \ (a \ y) is Element of the U1 of X
(a \ (a \ y)) \ (a \ x) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ y) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ a is Element of the U1 of X
x \ (a \ a) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ (0. X) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
a \ x is Element of the U1 of X
x \ (a \ y) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
y \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ x)) \ x is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
the U1 of BCI-EXAMPLE is non empty V12() V28() set
the Element of the U1 of BCI-EXAMPLE is Element of the U1 of BCI-EXAMPLE
0. BCI-EXAMPLE is V44( BCI-EXAMPLE ) Element of the U1 of BCI-EXAMPLE
x is Element of the U1 of BCI-EXAMPLE
x \ the Element of the U1 of BCI-EXAMPLE is Element of the U1 of BCI-EXAMPLE
y is Element of the U1 of BCI-EXAMPLE
the Element of the U1 of BCI-EXAMPLE \ y is Element of the U1 of BCI-EXAMPLE
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
K19( the U1 of X) is set
0. X is V44(X) Element of the U1 of X
BCK-part X is non empty Element of K19( the U1 of X)
{ b₁ where b₁ is Element of the U1 of X : 0. X <= b₁ } is set
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
z is Element of the U1 of X
(x \ y) \ z is Element of the U1 of X
y \ x is Element of the U1 of X
y \ (y \ x) is Element of the U1 of X
x \ (y \ (y \ x)) is Element of the U1 of X
(0. X) \ (x \ (y \ (y \ x))) is Element of the U1 of X
(x \ (y \ (y \ x))) ` is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
K19( the U1 of X) is set
a is non empty Element of K19( the U1 of X)
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
y \ x is Element of the U1 of X
y \ (y \ x) is Element of the U1 of X
x \ (y \ (y \ x)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(x \ y) \ (0. X) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
K19( the U1 of X) is set
a is non empty Element of K19( the U1 of X)
x is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of x is non empty set
y is Element of the U1 of x
z is Element of the U1 of x
y \ z is Element of the U1 of x
0. x is V44(x) Element of the U1 of x
(0. x) \ y is Element of the U1 of x
(0. x) \ ((0. x) \ y) is Element of the U1 of x
y \ ((0. x) \ ((0. x) \ y)) is Element of the U1 of x
y ` is Element of the U1 of x
(0. x) \ (y `) is Element of the U1 of x
y \ ((0. x) \ (y `)) is Element of the U1 of x
(0. x) \ (0. x) is Element of the U1 of x
y \ ((0. x) \ (0. x)) is Element of the U1 of x
y \ (0. x) is Element of the U1 of x
(y \ (0. x)) \ z is Element of the U1 of x
0. x is V44(x) Element of the U1 of x
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
K19( the U1 of X) is set
a is non empty Element of K19( the U1 of X)
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
x \ (x \ y) is Element of the U1 of X
y \ x is Element of the U1 of X
y \ (y \ x) is Element of the U1 of X
(y \ (y \ x)) \ (x \ y) is Element of the U1 of X
((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) is Element of the U1 of X
y \ (x \ y) is Element of the U1 of X
(y \ (x \ y)) \ (y \ x) is Element of the U1 of X
((y \ (x \ y)) \ (y \ x)) \ (x \ (x \ y)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
the U1 of BCI-EXAMPLE is non empty V12() V28() set
a is Element of the U1 of BCI-EXAMPLE
x is Element of the U1 of BCI-EXAMPLE
a \ x is Element of the U1 of BCI-EXAMPLE
y is Element of the U1 of BCI-EXAMPLE
(a \ x) \ y is Element of the U1 of BCI-EXAMPLE
a \ y is Element of the U1 of BCI-EXAMPLE
x \ y is Element of the U1 of BCI-EXAMPLE
(a \ y) \ (x \ y) is Element of the U1 of BCI-EXAMPLE
the U1 of BCI-EXAMPLE is non empty V12() V28() set
a is Element of the U1 of BCI-EXAMPLE
x is Element of the U1 of BCI-EXAMPLE
x \ a is Element of the U1 of BCI-EXAMPLE
a \ (x \ a) is Element of the U1 of BCI-EXAMPLE
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(a \ x) \ (x \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(a \ x) \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
y is Element of the U1 of X
(a \ x) \ y is Element of the U1 of X
a \ y is Element of the U1 of X
x \ y is Element of the U1 of X
(a \ y) \ (x \ y) is Element of the U1 of X
(x \ y) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ y is Element of the U1 of X
y ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ y is Element of the U1 of X
(a \ y) \ x is Element of the U1 of X
((a \ y) \ x) \ ((a \ y) \ (x \ y)) is Element of the U1 of X
((a \ x) \ y) \ ((a \ y) \ (x \ y)) is Element of the U1 of X
((a \ y) \ (x \ y)) \ ((a \ x) \ y) is Element of the U1 of X
(a \ y) \ y is Element of the U1 of X
((a \ y) \ y) \ (x \ y) is Element of the U1 of X
(((a \ y) \ y) \ (x \ y)) \ ((a \ x) \ y) is Element of the U1 of X
(((a \ y) \ y) \ (x \ y)) \ ((a \ y) \ x) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
(a \ (a \ x)) \ (x \ a) is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a \ (a \ (x \ (x \ a))) is Element of the U1 of X
(a \ (a \ x)) \ x is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(a \ (a \ x)) \ (x \ (x \ a)) is Element of the U1 of X
x \ (x \ (x \ a)) is Element of the U1 of X
(a \ (a \ x)) \ (a \ (a \ (x \ (x \ a)))) is Element of the U1 of X
a \ (a \ (a \ (x \ (x \ a)))) is Element of the U1 of X
(a \ (a \ (a \ (x \ (x \ a))))) \ (a \ x) is Element of the U1 of X
(a \ (x \ (x \ a))) \ (a \ x) is Element of the U1 of X
((a \ (a \ x)) \ (a \ (a \ (x \ (x \ a))))) \ (x \ a) is Element of the U1 of X
((a \ (a \ x)) \ (x \ a)) \ (a \ (a \ (x \ (x \ a)))) is Element of the U1 of X
(x \ (x \ a)) \ a is Element of the U1 of X
(x \ a) \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (x \ a) is Element of the U1 of X
a \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (a \ (x \ a)) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ (x \ (x \ a)) is Element of the U1 of X
(a \ (x \ (x \ a))) \ (a \ (x \ (x \ a))) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ (a \ (x \ a)) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ (a \ (x \ (x \ a))) is Element of the U1 of X
(a \ (x \ a)) \ (a \ (x \ (x \ a))) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ (x \ a) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ ((a \ (a \ (x \ (x \ a)))) \ (x \ a)) is Element of the U1 of X
(x \ (x \ a)) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ (x \ a) is Element of the U1 of X
(x \ a) ` is Element of the U1 of X
(0. X) \ (x \ a) is Element of the U1 of X
((a \ (a \ (x \ (x \ a)))) \ (x \ a)) \ ((a \ (a \ x)) \ (x \ a)) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ ((a \ (a \ x)) \ (x \ a)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
(a \ (a \ x)) \ (x \ a) is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a \ (a \ (x \ (x \ a))) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (a \ (a \ (a \ x))) is Element of the U1 of X
(a \ x) \ ((a \ x) \ (a \ (a \ (a \ x)))) is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
(a \ x) \ ((a \ x) \ (a \ x)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(a \ x) \ (0. X) is Element of the U1 of X
(a \ x) \ a is Element of the U1 of X
(a \ x) \ ((a \ x) \ a) is Element of the U1 of X
((a \ x) \ ((a \ x) \ a)) \ (a \ (a \ x)) is Element of the U1 of X
a \ a is Element of the U1 of X
(a \ a) \ x is Element of the U1 of X
(a \ x) \ ((a \ a) \ x) is Element of the U1 of X
((a \ x) \ ((a \ a) \ x)) \ (a \ (a \ x)) is Element of the U1 of X
x ` is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
(a \ x) \ (x `) is Element of the U1 of X
((a \ x) \ (x `)) \ (a \ (a \ x)) is Element of the U1 of X
((a \ x) \ (0. X)) \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ (a \ x))) \ x is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ x) \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ a is Element of the U1 of X
(a \ x) \ ((a \ x) \ a) is Element of the U1 of X
((a \ x) \ ((a \ x) \ a)) \ (a \ (a \ x)) is Element of the U1 of X
a \ a is Element of the U1 of X
(a \ a) \ x is Element of the U1 of X
(a \ x) \ ((a \ a) \ x) is Element of the U1 of X
((a \ x) \ ((a \ a) \ x)) \ (a \ (a \ x)) is Element of the U1 of X
x ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ x is Element of the U1 of X
(a \ x) \ (x `) is Element of the U1 of X
((a \ x) \ (x `)) \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (0. X) is Element of the U1 of X
((a \ x) \ (0. X)) \ (a \ (a \ x)) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (a \ (a \ (a \ x))) is Element of the U1 of X
(a \ x) \ ((a \ x) \ (a \ (a \ (a \ x)))) is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
(a \ x) \ ((a \ x) \ (a \ x)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ x) \ (a \ (a \ x)) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ (a \ x))) \ x is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
x is Element of the U1 of X
x \ y is Element of the U1 of X
(a \ y) \ (x \ y) is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ y is Element of the U1 of X
((a \ y) \ (x \ y)) \ ((a \ x) \ y) is Element of the U1 of X
((a \ y) \ (x \ y)) \ ((a \ y) \ (x \ y)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
y is Element of the U1 of X
(a \ x) \ y is Element of the U1 of X
a \ y is Element of the U1 of X
x \ y is Element of the U1 of X
(a \ y) \ (x \ y) is Element of the U1 of X
(x \ y) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ y is Element of the U1 of X
y ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ y is Element of the U1 of X
a \ (x \ y) is Element of the U1 of X
(a \ (x \ y)) \ y is Element of the U1 of X
((a \ x) \ y) \ ((a \ (x \ y)) \ y) is Element of the U1 of X
((a \ x) \ y) \ ((a \ y) \ (x \ y)) is Element of the U1 of X
((a \ y) \ (x \ y)) \ ((a \ x) \ y) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
((a \ x) \ x) \ ((a \ x) \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
((a \ x) \ x) \ (a \ x) is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
((a \ x) \ (a \ x)) \ x is Element of the U1 of X
x ` is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a \ (a \ (x \ (x \ a))) is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (x \ a) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ ((a \ (a \ x)) \ (x \ a)) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ (a \ (a \ (x \ (x \ a)))) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
(a \ (a \ x)) \ (x \ a) is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ (x \ (x \ a)) is Element of the U1 of X
a \ (a \ (x \ (x \ a))) is Element of the U1 of X
(a \ (a \ (x \ (x \ a)))) \ ((a \ (a \ x)) \ (x \ a)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
((a \ (a \ x)) \ (x \ a)) \ (a \ (a \ (x \ (x \ a)))) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(a \ (a \ x)) \ x is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(a \ (a \ x)) \ (x \ a) is Element of the U1 of X
a \ (x \ a) is Element of the U1 of X
(a \ (x \ a)) \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
(a \ x) \ (x \ (a \ x)) is Element of the U1 of X
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
a \ (x \ a) is Element of the U1 of X
a \ (a \ (x \ a)) is Element of the U1 of X
a \ (a \ (a \ (x \ a))) is Element of the U1 of X
(x \ a) \ a is Element of the U1 of X
(x \ a) \ ((x \ a) \ a) is Element of the U1 of X
a \ ((x \ a) \ ((x \ a) \ a)) is Element of the U1 of X
(x \ a) \ (x \ a) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (a \ x) is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
(x \ (a \ x)) \ (x \ a) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ (a \ x))) \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ (a \ x))) \ x is Element of the U1 of X
(a \ x) \ a is Element of the U1 of X
a \ a is Element of the U1 of X
(a \ a) \ x is Element of the U1 of X
x ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ a) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ x is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (0. X) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
X is non empty BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
a \ ((0. X) \ x) is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ y) \ (a \ x) is Element of the U1 of X
x \ y is Element of the U1 of X
x \ a is Element of the U1 of X
(x \ y) \ (x \ a) is Element of the U1 of X
((x \ y) \ (x \ a)) \ (a \ x) is Element of the U1 of X
x ` is Element of the U1 of X
a \ (x `) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(x \ y) \ (a \ x) is Element of the U1 of X
((x \ y) \ (a \ x)) \ (x \ a) is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
(x \ (a \ x)) \ y is Element of the U1 of X
((x \ (a \ x)) \ y) \ (x \ a) is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ y is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ y is Element of the U1 of X
a is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(0. X) \ (0. X) is Element of the U1 of X
(0. X) \ ((0. X) \ (0. X)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ a is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (0. X) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
(x \ (0. X)) \ (0. X) is Element of the U1 of X
((x \ (0. X)) \ (0. X)) \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (a \ x) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (a \ x) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
(x \ (0. X)) \ (x \ a) is Element of the U1 of X
((x \ (0. X)) \ (x \ a)) \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
a \ a is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
(0. X) \ ((0. X) \ a) is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
a \ (a \ (0. X)) is Element of the U1 of X
(a \ (a \ (0. X))) \ ((0. X) \ a) is Element of the U1 of X
(a \ a) \ ((0. X) \ a) is Element of the U1 of X
a is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
((0. X) \ a) \ ((0. X) \ a) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ a is Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ x) \ (a \ (0. X)) is Element of the U1 of X
(0. X) \ x is Element of the U1 of X
(0. X) \ a is Element of the U1 of X
((0. X) \ x) \ ((0. X) \ a) is Element of the U1 of X
(((0. X) \ x) \ ((0. X) \ a)) \ (a \ (0. X)) is Element of the U1 of X
(0. X) \ ((0. X) \ a) is Element of the U1 of X
((0. X) \ ((0. X) \ a)) \ (a \ (0. X)) is Element of the U1 of X
(0. X) \ (a \ (0. X)) is Element of the U1 of X
a is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ y) \ (a \ x) is Element of the U1 of X
x \ y is Element of the U1 of X
x \ a is Element of the U1 of X
(x \ y) \ (x \ a) is Element of the U1 of X
((a \ y) \ (a \ x)) \ ((x \ y) \ (x \ a)) is Element of the U1 of X
((x \ y) \ (x \ a)) \ (a \ x) is Element of the U1 of X
(((x \ y) \ (x \ a)) \ (a \ x)) \ ((x \ y) \ (x \ a)) is Element of the U1 of X
a is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ y) \ (a \ x) is Element of the U1 of X
x \ y is Element of the U1 of X
x \ a is Element of the U1 of X
(x \ y) \ (x \ a) is Element of the U1 of X
((x \ y) \ (x \ a)) \ ((a \ y) \ (a \ x)) is Element of the U1 of X
((a \ y) \ (a \ x)) \ ((x \ y) \ (x \ a)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ (0. X) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
x \ (x \ y) is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
y \ x is Element of the U1 of X
x \ (y \ x) is Element of the U1 of X
y \ a is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a \ x is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
x \ (x \ (y \ x)) is Element of the U1 of X
(x \ (y \ x)) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ (y \ x) is Element of the U1 of X
(y \ x) ` is Element of the U1 of X
(0. X) \ (y \ x) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
a \ (x \ a) is Element of the U1 of X
a \ (a \ (x \ a)) is Element of the U1 of X
a \ a is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
a \ (x \ a) is Element of the U1 of X
(a \ (x \ a)) \ a is Element of the U1 of X
a \ a is Element of the U1 of X
(a \ a) \ (x \ a) is Element of the U1 of X
(x \ a) ` is Element of the U1 of X
(0. X) \ (x \ a) is Element of the U1 of X
a \ (a \ (x \ a)) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
x \ (x \ (x \ a)) is Element of the U1 of X
x \ (x \ (x \ (x \ a))) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (a \ (a \ (a \ x))) is Element of the U1 of X
(a \ x) \ ((a \ x) \ (a \ (a \ (a \ x)))) is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
(a \ x) \ ((a \ x) \ (a \ x)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(a \ x) \ (0. X) is Element of the U1 of X
(a \ (a \ (a \ x))) \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ (a \ x))) \ x is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
x \ (a \ (a \ x)) is Element of the U1 of X
x \ (x \ (a \ (a \ x))) is Element of the U1 of X
x \ (x \ (x \ a)) is Element of the U1 of X
x \ (x \ (x \ (x \ a))) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ y) \ (a \ x) is Element of the U1 of X
x \ y is Element of the U1 of X
x \ a is Element of the U1 of X
(x \ a) \ y is Element of the U1 of X
(x \ y) \ ((x \ a) \ y) is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ y is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ y is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (a \ x) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
(x \ a) \ (0. X) is Element of the U1 of X
(x \ (0. X)) \ ((x \ a) \ (0. X)) is Element of the U1 of X
x \ ((x \ a) \ (0. X)) is Element of the U1 of X
x is Element of the U1 of X
a is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (x \ a) is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (x \ a) is Element of the U1 of X
(a \ (x \ a)) \ (a \ x) is Element of the U1 of X
(x \ a) \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ ((x \ a) \ (x \ a)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(x \ (x \ a)) \ (0. X) is Element of the U1 of X
(a \ (a \ x)) \ (x \ a) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
a \ (x \ y) is Element of the U1 of X
a \ (a \ (x \ y)) is Element of the U1 of X
a \ y is Element of the U1 of X
(x \ y) \ (a \ y) is Element of the U1 of X
(x \ y) \ ((x \ y) \ (a \ y)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(a \ (0. X)) \ (a \ (x \ y)) is Element of the U1 of X
(x \ y) \ (0. X) is Element of the U1 of X
(x \ y) \ a is Element of the U1 of X
((x \ y) \ a) \ (0. X) is Element of the U1 of X
((x \ y) \ (0. X)) \ (((x \ y) \ a) \ (0. X)) is Element of the U1 of X
(x \ y) \ (((x \ y) \ a) \ (0. X)) is Element of the U1 of X
(x \ y) \ ((x \ y) \ a) is Element of the U1 of X
x \ a is Element of the U1 of X
(x \ a) \ y is Element of the U1 of X
(x \ y) \ ((x \ a) \ y) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
x \ y is Element of the U1 of X
a \ (x \ y) is Element of the U1 of X
a \ (a \ (x \ y)) is Element of the U1 of X
a \ y is Element of the U1 of X
(x \ y) \ (a \ y) is Element of the U1 of X
(x \ y) \ ((x \ y) \ (a \ y)) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
a \ (x \ a) is Element of the U1 of X
a \ (a \ (x \ a)) is Element of the U1 of X
a \ a is Element of the U1 of X
(x \ a) \ (a \ a) is Element of the U1 of X
(x \ a) \ ((x \ a) \ (a \ a)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(x \ a) \ (0. X) is Element of the U1 of X
(x \ a) \ ((x \ a) \ (0. X)) is Element of the U1 of X
(x \ a) \ (x \ a) is Element of the U1 of X
(a \ (x \ a)) \ a is Element of the U1 of X
(a \ a) \ (x \ a) is Element of the U1 of X
(x \ a) ` is Element of the U1 of X
(0. X) \ (x \ a) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (a \ x) is Element of the U1 of X
(a \ (a \ x)) \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
(x \ (x \ a)) \ (a \ x) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
x \ a is Element of the U1 of X
x \ (x \ a) is Element of the U1 of X
a \ x is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
a \ (0. X) is Element of the U1 of X
(x \ (x \ a)) \ (0. X) is Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ a is Element of the U1 of X
a \ a is Element of the U1 of X
(a \ a) \ x is Element of the U1 of X
x ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ x is Element of the U1 of X
a \ (a \ x) is Element of the U1 of X
a \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ ((a \ x) \ a) is Element of the U1 of X
((a \ x) \ ((a \ x) \ a)) \ (a \ (a \ x)) is Element of the U1 of X
(a \ x) \ (a \ (a \ x)) is Element of the U1 of X
(a \ (a \ (a \ x))) \ x is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () () BCIStr_0
the U1 of X is non empty set
0. X is V44(X) Element of the U1 of X
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
x \ (x \ (a \ x)) is Element of the U1 of X
x \ x is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
y \ x is Element of the U1 of X
x \ (y \ x) is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
x \ (x \ (a \ x)) is Element of the U1 of X
y \ a is Element of the U1 of X
(x \ (a \ x)) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ (a \ x) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
x \ (x \ (y \ x)) is Element of the U1 of X
(x \ (y \ x)) \ x is Element of the U1 of X
(x \ x) \ (y \ x) is Element of the U1 of X
(y \ x) ` is Element of the U1 of X
(0. X) \ (y \ x) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ (x \ (a \ x)) is Element of the U1 of X
(x \ (a \ x)) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ (a \ x) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
y \ x is Element of the U1 of X
x \ (y \ x) is Element of the U1 of X
a \ x is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
(x \ (a \ x)) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ (a \ x) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
y \ a is Element of the U1 of X
x \ (x \ (a \ x)) is Element of the U1 of X
x \ (x \ (y \ x)) is Element of the U1 of X
(x \ (y \ x)) \ x is Element of the U1 of X
(x \ x) \ (y \ x) is Element of the U1 of X
(y \ x) ` is Element of the U1 of X
(0. X) \ (y \ x) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
((a \ x) \ x) \ (a \ x) is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
((a \ x) \ (a \ x)) \ x is Element of the U1 of X
x ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
y \ x is Element of the U1 of X
x \ (y \ x) is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
(a \ x) \ (a \ x) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
x \ (x \ (a \ x)) is Element of the U1 of X
y \ a is Element of the U1 of X
(x \ (a \ x)) \ x is Element of the U1 of X
x \ x is Element of the U1 of X
(x \ x) \ (a \ x) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
x \ (x \ (y \ x)) is Element of the U1 of X
(x \ (y \ x)) \ x is Element of the U1 of X
(x \ x) \ (y \ x) is Element of the U1 of X
(y \ x) ` is Element of the U1 of X
(0. X) \ (y \ x) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
x is Element of the U1 of X
(a \ y) \ x is Element of the U1 of X
(a \ y) \ ((a \ y) \ x) is Element of the U1 of X
x \ y is Element of the U1 of X
x \ (a \ y) is Element of the U1 of X
a \ x is Element of the U1 of X
y \ (a \ x) is Element of the U1 of X
x \ (x \ (a \ y)) is Element of the U1 of X
(y \ (a \ x)) \ y is Element of the U1 of X
y \ y is Element of the U1 of X
(y \ y) \ (a \ x) is Element of the U1 of X
(a \ x) ` is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
(0. X) \ (a \ x) is Element of the U1 of X
(x \ y) \ ((a \ y) \ ((a \ y) \ x)) is Element of the U1 of X
(a \ y) \ y is Element of the U1 of X
((a \ y) \ ((a \ y) \ x)) \ (x \ y) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
x \ x is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
y is Element of the U1 of X
x is Element of the U1 of X
y \ x is Element of the U1 of X
y \ (y \ x) is Element of the U1 of X
a \ y is Element of the U1 of X
x \ (a \ y) is Element of the U1 of X
x \ y is Element of the U1 of X
x \ (x \ y) is Element of the U1 of X
(a \ y) \ x is Element of the U1 of X
(a \ y) \ ((a \ y) \ x) is Element of the U1 of X
x \ ((a \ y) \ ((a \ y) \ x)) is Element of the U1 of X
x \ (x \ (a \ y)) is Element of the U1 of X
x \ (x \ (x \ (a \ y))) is Element of the U1 of X
y is Element of the U1 of X
a \ y is Element of the U1 of X
x is Element of the U1 of X
(a \ y) \ x is Element of the U1 of X
(a \ y) \ ((a \ y) \ x) is Element of the U1 of X
x \ y is Element of the U1 of X
a \ (a \ y) is Element of the U1 of X
x \ (a \ (a \ y)) is Element of the U1 of X
y \ a is Element of the U1 of X
y \ (y \ a) is Element of the U1 of X
x \ (y \ (y \ a)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
y \ (0. X) is Element of the U1 of X
x \ (y \ (0. X)) is Element of the U1 of X
X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 () () BCIStr_0
the U1 of X is non empty set
a is Element of the U1 of X
x is Element of the U1 of X
y is Element of the U1 of X
z is Element of the U1 of X
y \ z is Element of the U1 of X
x \ (y \ z) is Element of the U1 of X
x \ y is Element of the U1 of X
(x \ (y \ z)) \ (x \ y) is Element of the U1 of X
a \ z is Element of the U1 of X
x \ (a \ z) is Element of the U1 of X
x \ z is Element of the U1 of X
x \ (x \ z) is Element of the U1 of X
(x \ (y \ z)) \ (x \ (x \ z)) is Element of the U1 of X
(x \ y) \ z is Element of the U1 of X
((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ y) \ z) is Element of the U1 of X
(x \ z) \ (y \ z) is Element of the U1 of X
((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ z) \ (y \ z)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
((x \ y) \ z) \ (x \ y) is Element of the U1 of X
(x \ y) \ (x \ y) is Element of the U1 of X
((x \ y) \ (x \ y)) \ z is Element of the U1 of X
z ` is Element of the U1 of X
(0. X) \ z is Element of the U1 of X
((x \ (y \ z)) \ (x \ (x \ z))) \ (x \ y) is Element of the U1 of X
((x \ (y \ z)) \ (x \ y)) \ (x \ (a \ z)) is Element of the U1 of X
z \ x is Element of the U1 of X
z \ (z \ x) is Element of the U1 of X
((x \ (y \ z)) \ (x \ y)) \ (z \ (z \ x)) is Element of the U1 of X
((x \ (y \ z)) \ (x \ y)) \ (x \ (x \ z)) is Element of the U1 of X
0. X is V44(X) Element of the U1 of X
x is Element of the U1 of X
a \ x is Element of the U1 of X
(a \ x) \ x is Element of the U1 of X
(a \ x) \ ((a \ x) \ x) is Element of the U1 of X
x \ x is Element of the U1 of X
x \ (x \ x) is Element of the U1 of X
(x \ (x \ x)) \ (x \ x) is Element of the U1 of X
x \ (a \ x) is Element of the U1 of X
x \ (0. X) is Element of the U1 of X
(x \ (0. X)) \ (x \ x) is Element of the U1 of X
x \ (x \ (a \ x)) is Element of the U1 of X