:: 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

a is Element of AtomSet X

BranchV a is non empty Element of K19( the U1 of X)

{ b

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

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

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

c

c

c

c

c

c

c

c

c

c

(c

c

((c

c

c

c

c

c

c

c

c

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

c

c

c

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

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