:: BCIIDEAL semantic presentation

K87() is set

K19(K87()) is set

K110() is set

K19(K110()) is set

K114() is Element of K19(K110())

{} is set

the empty set is empty set

1 is non empty set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

y \ I is Element of the carrier of X

y \ (y \ I) is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

I \ (x \ y) is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

I \ (x \ y) is Element of the carrier of X

(I \ (x \ y)) \ (I \ (x \ y)) is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (x \ y) is Element of the carrier of X

((I \ (x \ y)) \ (I \ (x \ y))) \ ((x \ y) \ (x \ y)) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

((I \ (x \ y)) \ (I \ (x \ y))) \ (y \ y) is Element of the carrier of X

((x \ y) \ (x \ y)) \ (y \ y) is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

((x \ y) \ (y \ y)) \ (x \ y) is Element of the carrier of X

(((I \ (x \ y)) \ (I \ (x \ y))) \ (y \ y)) \ (0. X) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ (y \ y) is Element of the carrier of X

I \ (x \ (y \ y)) is Element of the carrier of X

x is Element of the carrier of X

y \ x is Element of the carrier of X

x \ (y \ x) is Element of the carrier of X

I \ (x \ (y \ x)) is Element of the carrier of X

(I \ (x \ (y \ y))) \ (I \ (x \ (y \ x))) is Element of the carrier of X

x \ y is Element of the carrier of X

(x \ (y \ x)) \ (x \ (y \ y)) is Element of the carrier of X

((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ ((x \ (y \ x)) \ (x \ (y \ y))) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(y \ y) \ (y \ x) is Element of the carrier of X

((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ ((y \ y) \ (y \ x)) is Element of the carrier of X

((x \ (y \ x)) \ (x \ (y \ y))) \ ((y \ y) \ (y \ x)) is Element of the carrier of X

(x \ (y \ x)) \ ((y \ y) \ (y \ x)) is Element of the carrier of X

((x \ (y \ x)) \ ((y \ y) \ (y \ x))) \ (x \ (y \ y)) is Element of the carrier of X

(((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ ((y \ y) \ (y \ x))) \ (0. X) is Element of the carrier of X

((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ (x \ y) is Element of the carrier of X

((y \ y) \ (y \ x)) \ (x \ y) is Element of the carrier of X

(y \ y) \ (x \ y) is Element of the carrier of X

((y \ y) \ (x \ y)) \ (y \ x) is Element of the carrier of X

(((I \ (x \ (y \ y))) \ (I \ (x \ (y \ x)))) \ (x \ y)) \ (0. X) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

(0. X) \ (I \ x) is Element of the carrier of X

x \ I is Element of the carrier of X

((0. X) \ (I \ x)) \ (x \ I) is Element of the carrier of X

(0. X) \ I is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

((0. X) \ I) \ ((0. X) \ x) is Element of the carrier of X

(((0. X) \ I) \ ((0. X) \ x)) \ (x \ I) is Element of the carrier of X

((0. X) \ I) \ (x \ I) is Element of the carrier of X

(((0. X) \ I) \ (x \ I)) \ ((0. X) \ x) is Element of the carrier of X

(x \ I) ` is Element of the carrier of X

(0. X) \ (x \ I) is Element of the carrier of X

((x \ I) `) \ I is Element of the carrier of X

(((x \ I) `) \ I) \ ((0. X) \ x) is Element of the carrier of X

x ` is Element of the carrier of X

I ` is Element of the carrier of X

(x `) \ (I `) is Element of the carrier of X

((x `) \ (I `)) \ I is Element of the carrier of X

(((x `) \ (I `)) \ I) \ ((0. X) \ x) is Element of the carrier of X

(x `) \ I is Element of the carrier of X

((x `) \ I) \ (I `) is Element of the carrier of X

(((x `) \ I) \ (I `)) \ ((0. X) \ x) is Element of the carrier of X

((x `) \ I) \ (x `) is Element of the carrier of X

(((x `) \ I) \ (x `)) \ (I `) is Element of the carrier of X

(x `) \ (x `) is Element of the carrier of X

((x `) \ (x `)) \ I is Element of the carrier of X

(((x `) \ (x `)) \ I) \ (I `) is Element of the carrier of X

(I `) \ (I `) is Element of the carrier of X

(I \ x) ` is Element of the carrier of X

((I \ x) `) \ (x \ I) is Element of the carrier of X

(I `) \ (x `) is Element of the carrier of X

((I `) \ (x `)) \ (x \ I) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of I

x \ y is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

AtomSet X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

{ b

x is Element of AtomSet X

y is Element of AtomSet X

BranchV y is non empty Element of K19( the carrier of X)

{ b

y is Element of AtomSet X

y \ x is Element of AtomSet X

y \ y is Element of AtomSet X

y \ x is Element of AtomSet X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

AtomSet X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

{ b

x is Element of the carrier of X

y is Element of AtomSet X

y is Element of AtomSet X

BranchV y is non empty Element of K19( the carrier of X)

{ b

x \ y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ y is Element of AtomSet X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of I

(X,x) is set

{ b

y is set

y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

AtomSet X is non empty Element of K19( the carrier of X)

the carrier of X is non empty set

K19( the carrier of X) is set

{ b

BCK-part X is non empty Element of K19( the carrier of X)

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

{(0. X)} is set

(BCK-part X) /\ (AtomSet X) is Element of K19( the carrier of X)

y is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

y is Element of BCK-part X

y is Element of AtomSet X

y \ y is Element of the carrier of X

y is Element of BCK-part X

y is Element of AtomSet X

y \ y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

AtomSet X is non empty Element of K19( the carrier of X)

the carrier of X is non empty set

K19( the carrier of X) is set

{ b

x is Element of AtomSet X

x ` is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(0. X) \ x is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{(0. X)} is set

I is non empty Ideal of X

x is non empty Ideal of X

I /\ x is Element of K19( the carrier of X)

K19( the carrier of X) is set

y is Element of I

y is Element of x

y \ y is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

(y \ (y \ y)) \ y is Element of the carrier of X

(y \ (y \ y)) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

(y \ y) \ (y \ y) is Element of the carrier of X

(y \ y) ` is Element of the carrier of X

(0. X) \ (y \ y) is Element of the carrier of X

(y \ y) \ y is Element of the carrier of X

(y \ y) \ y is Element of the carrier of X

y ` is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

y is set

y is Element of I

x is Element of x

y \ x is Element of the carrier of X

y is set

X is non empty being_B being_C being_I being_BCI-4 associative weakly-positive-implicative V67() alternative BCIStr_0

I is non empty Ideal of X

the carrier of X is non empty set

x is Element of I

x ` is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(0. X) \ x is Element of the carrier of X

x \ (0. X) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

I is non empty Ideal of X

the carrier of X is non empty set

x is Element of I

x ` is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(0. X) \ x is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is set

K19( the carrier of X) is set

x is non empty Ideal of X

y is Element of the carrier of X

y is Element of the carrier of X

x is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

x is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

K19( the carrier of X) is set

I is non empty Element of K19( the carrier of X)

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(x \ y) \ (0. X) is Element of the carrier of X

y \ (0. X) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ (y \ y) is Element of the carrier of X

x \ (x \ y) is Element of the carrier of X

(x \ (x \ y)) \ y is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(x \ (x \ y)) \ (y \ y) is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

((x \ (x \ y)) \ (y \ y)) \ y is Element of the carrier of X

(y \ (y \ y)) \ y is Element of the carrier of X

(((x \ (x \ y)) \ (y \ y)) \ y) \ (0. X) is Element of the carrier of X

(x \ (y \ y)) \ (x \ y) is Element of the carrier of X

((x \ (y \ y)) \ (x \ y)) \ y is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ (y \ y) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is non empty Ideal of X

x is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

x \ ((0. X) \ x) is Element of the carrier of X

x \ x is Element of the carrier of X

x \ (0. X) is Element of the carrier of X

(x \ (0. X)) \ x is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is non empty Ideal of X

x is Element of I

x ` is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

((0. X) \ x) \ x is Element of the carrier of X

(0. X) \ ((0. X) \ x) is Element of the carrier of X

(0. X) \ ((0. X) \ ((0. X) \ x)) is Element of the carrier of X

((0. X) \ ((0. X) \ ((0. X) \ x))) \ x is Element of the carrier of X

((0. X) \ x) \ ((0. X) \ ((0. X) \ x)) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

K19( the carrier of X) is set

I is non empty Element of K19( the carrier of X)

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

x \ (0. X) is Element of the carrier of X

(x \ (0. X)) \ y is Element of the carrier of X

y \ (0. X) is Element of the carrier of X

(x \ (0. X)) \ (y \ (0. X)) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

BCK-part X is non empty Element of K19( the carrier of X)

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

I is non empty Ideal of X

x is set

y is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

y is Element of the carrier of X

(0. X) \ ((0. X) \ y) is Element of the carrier of X

y \ y is Element of the carrier of X

(y \ y) \ ((0. X) \ y) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

BCK-part X is non empty Element of K19( the carrier of X)

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

((x \ y) \ (y \ y)) ` is Element of the carrier of X

(0. X) \ ((x \ y) \ (y \ y)) is Element of the carrier of X

x is Element of the carrier of X

(x \ y) ` is Element of the carrier of X

(0. X) \ (x \ y) is Element of the carrier of X

(y \ y) ` is Element of the carrier of X

(0. X) \ (y \ y) is Element of the carrier of X

((x \ y) `) \ ((y \ y) `) is Element of the carrier of X

x ` is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

y ` is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

(x `) \ (y `) is Element of the carrier of X

((x `) \ (y `)) \ ((y \ y) `) is Element of the carrier of X

y ` is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

x is Element of the carrier of X

(0. X) \ (y `) is Element of the carrier of X

((x `) \ (y `)) \ ((0. X) \ (y `)) is Element of the carrier of X

(x `) \ (0. X) is Element of the carrier of X

(((x `) \ (y `)) \ ((0. X) \ (y `))) \ ((x `) \ (0. X)) is Element of the carrier of X

((x `) \ (0. X)) ` is Element of the carrier of X

(0. X) \ ((x `) \ (0. X)) is Element of the carrier of X

(x `) ` is Element of the carrier of X

(0. X) \ (x `) is Element of the carrier of X

(0. X) \ ((0. X) \ x) is Element of the carrier of X

(0. X) \ (0. X) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ x is Element of the carrier of X

(y \ x) ` is Element of the carrier of X

(0. X) \ (y \ x) is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

x \ y is Element of the carrier of X

((x \ y) \ (y \ y)) \ (x \ y) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

((x \ y) \ (y \ y)) \ (x \ y) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

x \ y is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

BCK-part X is non empty Element of K19( the carrier of X)

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y ` is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) ` is Element of the carrier of X

(0. X) \ (x \ y) is Element of the carrier of X

y is Element of the carrier of X

x ` is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

(x `) \ (0. X) is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

x \ (y \ (y \ x)) is Element of the carrier of X

(0. X) \ (x \ (y \ (y \ x))) is Element of the carrier of X

(x \ (y \ (y \ x))) ` is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

BCK-part X is non empty Element of K19( the carrier of X)

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

(x \ y) ` is Element of the carrier of X

(0. X) \ (x \ y) is Element of the carrier of X

y is Element of the carrier of X

x ` is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

y ` is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

(x `) \ (y `) is Element of the carrier of X

(x `) \ (0. X) is Element of the carrier of X

y is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

x \ (y \ (y \ x)) is Element of the carrier of X

(0. X) \ (x \ (y \ (y \ x))) is Element of the carrier of X

(x \ (y \ (y \ x))) ` is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

x is set

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

x is non empty Ideal of X

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

x is Element of the carrier of X

(y \ y) \ x is Element of the carrier of X

y \ y is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

y \ (y \ (y \ y)) is Element of the carrier of X

y \ (0. X) is Element of the carrier of X

y \ (y \ (0. X)) is Element of the carrier of X

y \ y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

I is set

x is Element of the carrier of X

x ` is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

BCK-part X is non empty Element of K19( the carrier of X)

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

BCK-part X is non empty Element of K19( the carrier of X)

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

{ b

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

(x \ y) ` is Element of the carrier of X

(0. X) \ (x \ y) is Element of the carrier of X

y is Element of the carrier of X

x ` is Element of the carrier of X

(0. X) \ x is Element of the carrier of X

y ` is Element of the carrier of X

(0. X) \ y is Element of the carrier of X

(x `) \ (y `) is Element of the carrier of X

(x `) \ (0. X) is Element of the carrier of X

y is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

x \ (y \ (y \ x)) is Element of the carrier of X

(0. X) \ (x \ (y \ (y \ x))) is Element of the carrier of X

(x \ (y \ (y \ x))) ` is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

x \ (y \ (y \ x)) is Element of the carrier of X

(x \ y) \ (0. X) is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

x \ (y \ (y \ x)) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

I is non empty Ideal of X

x is non empty Ideal of X

the carrier of X is non empty set

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

y \ y is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

y \ (y \ (y \ y)) is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

u is Element of the carrier of X

z is Element of the carrier of X

z \ x is Element of the carrier of X

u \ (z \ x) is Element of the carrier of X

z \ y is Element of the carrier of X

u \ (z \ y) is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

(y \ (y \ y)) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

(y \ y) \ (y \ y) is Element of the carrier of X

(y \ y) ` is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(0. X) \ (y \ y) is Element of the carrier of X

y \ (y \ (y \ y)) is Element of the carrier of X

y \ (y \ (y \ (y \ y))) is Element of the carrier of X

y \ (y \ (y \ (y \ (y \ y)))) is Element of the carrier of X

(y \ (y \ y)) \ y is Element of the carrier of X

(y \ y) \ (y \ y) is Element of the carrier of X

(y \ (y \ y)) \ (y \ (y \ (y \ (y \ y)))) is Element of the carrier of X

(y \ (y \ (y \ (y \ (y \ y))))) \ (y \ y) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is non empty Ideal of X

x is non empty Ideal of X

y is set

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I \ (x \ (x \ I)) is Element of the carrier of X

I \ (I \ x) is Element of the carrier of X

I \ (I \ (I \ x)) is Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I \ x is Element of the carrier of X

I \ (x \ (x \ I)) is Element of the carrier of X

(x \ (x \ I)) \ I is Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I \ (x \ (x \ I)) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is non empty Ideal of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is non empty Ideal of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

x \ (x \ y) is Element of the carrier of X

(x \ y) \ x is Element of the carrier of X

(x \ y) \ ((x \ y) \ x) is Element of the carrier of X

x \ ((x \ y) \ ((x \ y) \ x)) is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

(y \ (y \ x)) \ x is Element of the carrier of X

(y \ (y \ x)) \ (x \ y) is Element of the carrier of X

x \ x is Element of the carrier of X

(x \ x) \ y is Element of the carrier of X

(x \ y) \ ((x \ x) \ y) is Element of the carrier of X

x \ ((x \ x) \ y) is Element of the carrier of X

(x \ ((x \ x) \ y)) \ y is Element of the carrier of X

y ` is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(0. X) \ y is Element of the carrier of X

x \ (y `) is Element of the carrier of X

(x \ (y `)) \ y is Element of the carrier of X

x \ (0. X) is Element of the carrier of X

(x \ (0. X)) \ y is Element of the carrier of X

y \ (0. X) is Element of the carrier of X

(y \ (0. X)) \ (y \ x) is Element of the carrier of X

((y \ (0. X)) \ (y \ x)) \ (x \ (0. X)) is Element of the carrier of X

(y \ (y \ x)) \ (x \ (0. X)) is Element of the carrier of X

((y \ (0. X)) \ (y \ x)) \ (x \ y) is Element of the carrier of X

(x \ (0. X)) \ (x \ y) is Element of the carrier of X

((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

I \ (I \ x) is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I \ (x \ (x \ I)) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

I \ (I \ x) is Element of the carrier of X

x \ (I \ (I \ x)) is Element of the carrier of X

x \ (x \ (I \ (I \ x))) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is Element of the carrier of X

x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

0. X is V44(X) atom positive V87(X) Element of the carrier of X

the carrier of X is non empty set

{(0. X)} is set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

y \ y is Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

I is Element of the carrier of X

y \ I is Element of the carrier of X

y \ x is Element of the carrier of X

(y \ I) \ (y \ x) is Element of the carrier of X

x \ I is Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I \ (x \ (x \ I)) is Element of the carrier of X

I \ x is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

(y \ y) \ y is Element of the carrier of X

(y \ y) \ ((y \ y) \ y) is Element of the carrier of X

I is Element of the carrier of X

y is Element of the carrier of X

x is Element of the carrier of X

y \ x is Element of the carrier of X

y \ I is Element of the carrier of X

(y \ x) \ (y \ I) is Element of the carrier of X

(y \ x) \ ((y \ x) \ (y \ I)) is Element of the carrier of X

I \ x is Element of the carrier of X

(y \ x) \ (I \ x) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

I \ (I \ x) is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I is non empty Ideal of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I \ (x \ (x \ I)) is Element of the carrier of X

I is non empty Ideal of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

I \ (I \ x) is Element of the carrier of X

x \ (I \ (I \ x)) is Element of the carrier of X

x \ (x \ (I \ (I \ x))) is Element of the carrier of X

I is non empty Ideal of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is Element of the carrier of X

x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I is non empty Ideal of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

y \ y is Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

I \ x is Element of the carrier of X

x \ I is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

I is Element of the carrier of X

y \ I is Element of the carrier of X

y \ x is Element of the carrier of X

(y \ I) \ (y \ x) is Element of the carrier of X

x \ I is Element of the carrier of X

I is Element of the carrier of X

x is Element of the carrier of X

x \ I is Element of the carrier of X

x \ (x \ I) is Element of the carrier of X

I \ (x \ (x \ I)) is Element of the carrier of X

I \ x is Element of the carrier of X

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

(y \ y) \ y is Element of the carrier of X

(y \ y) \ ((y \ y) \ y) is Element of the carrier of X

I is Element of the carrier of X

y is Element of the carrier of X

x is Element of the carrier of X

y \ x is Element of the carrier of X

y \ I is Element of the carrier of X

(y \ x) \ (y \ I) is Element of the carrier of X

(y \ x) \ ((y \ x) \ (y \ I)) is Element of the carrier of X

I \ x is Element of the carrier of X

(y \ x) \ (I \ x) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

y \ x is Element of the carrier of X

x \ (y \ x) is Element of the carrier of X

y is Element of the carrier of X

(x \ (y \ x)) \ y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

y \ x is Element of the carrier of X

x \ (y \ x) is Element of the carrier of X

y is Element of the carrier of X

(x \ (y \ x)) \ y is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

y \ x is Element of the carrier of X

x \ (y \ x) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(x \ (y \ x)) \ (0. X) is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

y \ x is Element of the carrier of X

x \ (y \ x) is Element of the carrier of X

y is Element of the carrier of X

x is Element of the carrier of X

x \ y is Element of the carrier of X

y \ (x \ y) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

K19( the carrier of X) is set

0. X is V44(X) atom positive V87(X) Element of the carrier of X

I is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

((x \ y) \ y) \ ((x \ y) \ y) is Element of the carrier of X

(x \ y) \ (x \ y) is Element of the carrier of X

(((x \ y) \ y) \ ((x \ y) \ y)) \ ((x \ y) \ (x \ y)) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(((x \ y) \ y) \ ((x \ y) \ y)) \ (y \ y) is Element of the carrier of X

((x \ y) \ (x \ y)) \ (y \ y) is Element of the carrier of X

((((x \ y) \ y) \ ((x \ y) \ y)) \ (y \ y)) \ (0. X) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

x \ (y \ y) is Element of the carrier of X

(x \ (y \ y)) \ (x \ y) is Element of the carrier of X

y \ (y \ y) is Element of the carrier of X

((x \ (y \ y)) \ (x \ y)) \ (y \ (y \ y)) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

((x \ (y \ y)) \ (x \ y)) \ y is Element of the carrier of X

(y \ (y \ y)) \ y is Element of the carrier of X

(y \ y) \ (y \ y) is Element of the carrier of X

(((x \ (y \ y)) \ (x \ y)) \ y) \ (0. X) is Element of the carrier of X

(x \ (y \ y)) \ y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ y is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of X is non empty set

I is non empty Ideal of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

y \ y is Element of the carrier of X

x \ y is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ y is Element of the carrier of X

(x \ y) \ (y \ y) is Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

I is non empty Ideal of X

x is non empty Ideal of X

the carrier of X is non empty set

y is Element of the carrier of X

y is Element of the carrier of X

y \ y is Element of the carrier of X

(y \ y) \ y is Element of the carrier of X

y \ ((y \ y) \ y) is Element of the carrier of X

(y \ ((y \ y) \ y)) \ y is Element of the carrier of X

((y \ ((y \ y) \ y)) \ y) \ y is Element of the carrier of X

(y \ y) \ ((y \ y) \ y) is Element of the carrier of X

((y \ y) \ ((y \ y) \ y)) \ y is Element of the carrier of X

((y \ y) \ y) \ ((y \ y) \ y) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

I is non empty Ideal of X

the carrier of X is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

y \ x is Element of the carrier of X

y \ (y \ x) is Element of the carrier of X

x \ (y \ (y \ x)) is Element of the carrier of X

(x \ (y \ (y \ x))) \ x is Element of the carrier of X

x \ x is Element of the carrier of X

(x \ x) \ (y \ (y \ x)) is Element of the carrier of X

(y \ (y \ x)) ` is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X

(0. X) \ (y \ (y \ x)) is Element of the carrier of X

y \ (x \ (y \ (y \ x))) is Element of the carrier of X

(x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x)))) is Element of the carrier of X

(x \ (y \ (y \ x))) \ (y \ x) is Element of the carrier of X

((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y) is Element of the carrier of X

((x \ (y \ (y \ x))) \ (y \ x)) \ (x \ y) is Element of the carrier of X

x \ (y \ x) is Element of the carrier of X

(x \ (y \ x)) \ (y \ (y \ x)) is Element of the carrier of X

(((x \ (y \ (y \ x))) \ (y \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (0. X) is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

(x \ y) \ y is Element of the carrier of X

x \ (x \ y) is Element of the carrier of X

(x \ y) \ (x \ (x \ y)) is Element of the carrier of X

((x \ y) \ (x \ (x \ y))) \ ((x \ y) \ y) is Element of the carrier of X

0. X is V44(X) atom positive V87(X) Element of the carrier of X