:: MORPH_01 semantic presentation

K37() is V132() V133() V134() V138() set

K41() is V132() V133() V134() V135() V136() V137() V138() Element of K10(K37())

K10(K37()) is non empty set

K36() is V132() V133() V134() V135() V136() V137() V138() set

K10(K36()) is non empty set

K10(K41()) is non empty set

K11(K41(),K37()) is set

K10(K11(K41(),K37())) is non empty set

K38() is V132() V138() set

K39() is V132() V133() V134() V135() V138() set

K40() is V132() V133() V134() V135() V136() V138() set

K11(K37(),K37()) is set

K10(K11(K37(),K37())) is non empty set

{} is set

the empty V132() V133() V134() V135() V136() V137() V138() set is empty V132() V133() V134() V135() V136() V137() V138() set

1 is non empty V13() V14() V15() V117() V120() V121() V132() V133() V134() V135() V136() V137() Element of K41()

- 1 is V14() V15() V117() Element of K37()

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

B is Element of K10( the carrier of E)

C is Element of K10( the carrier of E)

{ b

( not b

A is set

X is Element of the carrier of E

C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of C is non empty set

K10( the carrier of C) is non empty set

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

B is Element of K10( the carrier of E)

C is Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (b

B + C is Element of K10( the carrier of E)

{ (b

(E,C,B) is Element of K10( the carrier of E)

{ b

( not b

A is set

X is Element of the carrier of E

A is Element of the carrier of E

X - A is Element of the carrier of E

- A is Element of the carrier of E

X + (- A) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is Element of K10( the carrier of E)

B is Element of K10( the carrier of E)

(E,B,C) is Element of K10( the carrier of E)

{ b

( not b

A is set

A is set

c is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

B is Element of K10( the carrier of E)

C is Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (b

B + C is Element of K10( the carrier of E)

{ (b

A is set

A is set

X is Element of the carrier of E

c is Element of the carrier of E

c - X is Element of the carrier of E

- X is Element of the carrier of E

c + (- X) is Element of the carrier of E

X + (c - X) is Element of the carrier of E

C + B is Element of K10( the carrier of E)

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

B is Element of K10( the carrier of E)

C is Element of K10( the carrier of E)

(E,B,C) is Element of K10( the carrier of E)

{ b

( not b

A is set

X is Element of the carrier of E

A is Element of the carrier of E

X - A is Element of the carrier of E

- A is Element of the carrier of E

X + (- A) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is Element of K10( the carrier of E)

B is Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (b

{ (b

union { (b

A is set

X is Element of the carrier of E

A is Element of the carrier of E

X + A is Element of the carrier of E

A + C is Element of K10( the carrier of E)

{ (A + b

A is set

X is set

A is Element of the carrier of E

A + C is Element of K10( the carrier of E)

{ (A + b

c is Element of the carrier of E

A + c is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,C,B) is Element of K10( the carrier of E)

{ b

( not b

{ (b

meet { (b

A is set

X is Element of the carrier of E

X + C is Element of K10( the carrier of E)

{ (X + b

A is set

c is Element of the carrier of E

b is set

c is Element of the carrier of E

c + C is Element of K10( the carrier of E)

{ (c + b

c - c is Element of the carrier of E

- c is Element of the carrier of E

c + (- c) is Element of the carrier of E

c + (c - c) is Element of the carrier of E

A is set

c is set

b is Element of the carrier of E

b + C is Element of K10( the carrier of E)

{ (b + b

c is Element of the carrier of E

g is Element of the carrier of E

c - g is Element of the carrier of E

- g is Element of the carrier of E

c + (- g) is Element of the carrier of E

g + C is Element of K10( the carrier of E)

{ (g + b

w is Element of the carrier of E

g + w is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (b

(- 1) (.) B is Element of K10( the carrier of E)

{ ((- 1) * b

{ b

A is set

X is Element of the carrier of E

A is Element of the carrier of E

X + A is Element of the carrier of E

c is Element of the carrier of E

c - A is Element of the carrier of E

- A is Element of the carrier of E

c + (- A) is Element of the carrier of E

(- 1) * A is Element of the carrier of E

c + ((- 1) * A) is Element of the carrier of E

c + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (c + b

(c + ((- 1) (.) B)) /\ C is Element of K10( the carrier of E)

A is set

X is Element of the carrier of E

X + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (X + b

(X + ((- 1) (.) B)) /\ C is Element of K10( the carrier of E)

A is set

c is Element of the carrier of E

X + c is Element of the carrier of E

b is Element of the carrier of E

(- 1) * b is Element of the carrier of E

c is Element of the carrier of E

c + b is Element of the carrier of E

X - b is Element of the carrier of E

- b is Element of the carrier of E

X + (- b) is Element of the carrier of E

(X - b) + b is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,C,B) is Element of K10( the carrier of E)

{ b

( not b

(- 1) (.) B is Element of K10( the carrier of E)

{ ((- 1) * b

{ b

A is set

X is Element of the carrier of E

X + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (X + b

A is set

c is Element of the carrier of E

X + c is Element of the carrier of E

b is Element of the carrier of E

(- 1) * b is Element of the carrier of E

X - b is Element of the carrier of E

- b is Element of the carrier of E

X + (- b) is Element of the carrier of E

A is set

X is Element of the carrier of E

X + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (X + b

A is Element of the carrier of E

X - A is Element of the carrier of E

- A is Element of the carrier of E

X + (- A) is Element of the carrier of E

(- 1) * A is Element of the carrier of E

X + ((- 1) * A) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

the carrier of E \ C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

( the carrier of E \ C) + B is Element of K10( the carrier of E)

{ (b

(E,C,B) is Element of K10( the carrier of E)

{ b

( not b

the carrier of E \ (E,C,B) is Element of K10( the carrier of E)

(E,( the carrier of E \ C),B) is Element of K10( the carrier of E)

{ b

( not b

C + B is Element of K10( the carrier of E)

{ (b

the carrier of E \ (C + B) is Element of K10( the carrier of E)

A is Element of K10( the carrier of E)

A + B is Element of K10( the carrier of E)

{ (b

the carrier of E \ the carrier of E is Element of K10( the carrier of E)

(E,A,B) is Element of K10( the carrier of E)

{ b

( not b

(- 1) (.) B is Element of K10( the carrier of E)

{ ((- 1) * b

{ b

{ b

A is set

X is Element of the carrier of E

X + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (X + b

(X + ((- 1) (.) B)) /\ ( the carrier of E \ C) is Element of K10( the carrier of E)

A is Element of the carrier of E

A + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (A + b

X is Element of the carrier of E

X + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (X + b

(X + ((- 1) (.) B)) /\ ( the carrier of E \ C) is Element of K10( the carrier of E)

(X + ((- 1) (.) B)) /\ the carrier of E is Element of K10( the carrier of E)

((X + ((- 1) (.) B)) /\ the carrier of E) \ C is Element of K10( the carrier of E)

(X + ((- 1) (.) B)) \ C is Element of K10( the carrier of E)

{ b

{ b

A is set

X is Element of the carrier of E

X + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (X + b

A is Element of the carrier of E

A + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (A + b

(A + ((- 1) (.) B)) /\ C is Element of K10( the carrier of E)

the carrier of E \ ( the carrier of E \ C) is Element of K10( the carrier of E)

the carrier of E /\ C is Element of K10( the carrier of E)

A is Element of the carrier of E

A + ((- 1) (.) B) is Element of K10( the carrier of E)

{ (A + b

(A + ((- 1) (.) B)) \ ( the carrier of E \ C) is Element of K10( the carrier of E)

(A + ((- 1) (.) B)) \ the carrier of E is Element of K10( the carrier of E)

(A + ((- 1) (.) B)) /\ C is Element of K10( the carrier of E)

((A + ((- 1) (.) B)) \ the carrier of E) \/ ((A + ((- 1) (.) B)) /\ C) is Element of K10( the carrier of E)

{} \/ ((A + ((- 1) (.) B)) /\ C) is set

the carrier of E \ { b

the carrier of E \ { b

E is non empty Abelian addLoopStr

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is Element of K10( the carrier of E)

B is Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (b

B + C is Element of K10( the carrier of E)

{ (b

B + C is Element of K10( the carrier of E)

E is non empty Abelian addLoopStr

the carrier of E is non empty set

K10( the carrier of E) is non empty set

A is Element of K10( the carrier of E)

X is Element of K10( the carrier of E)

A + X is Element of K10( the carrier of E)

{ (b

X + A is Element of K10( the carrier of E)

{ (b

E is non empty add-associative addLoopStr

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is Element of K10( the carrier of E)

B is Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (b

A is Element of K10( the carrier of E)

(C + B) + A is Element of K10( the carrier of E)

{ (b

B + A is Element of K10( the carrier of E)

{ (b

C + (B + A) is Element of K10( the carrier of E)

{ (b

X is Element of the carrier of E

A is Element of the carrier of E

c is Element of the carrier of E

A + c is Element of the carrier of E

b is Element of the carrier of E

c is Element of the carrier of E

b + c is Element of the carrier of E

c + c is Element of the carrier of E

b + (c + c) is Element of the carrier of E

A is Element of the carrier of E

c is Element of the carrier of E

A + c is Element of the carrier of E

b is Element of the carrier of E

c is Element of the carrier of E

b + c is Element of the carrier of E

A + b is Element of the carrier of E

(A + b) + c is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,C,B) is Element of K10( the carrier of E)

{ (b

A is non empty Element of K10( the carrier of E)

(E,(E,C,B),A) is Element of K10( the carrier of E)

{ (b

(E,B,A) is Element of K10( the carrier of E)

{ (b

(E,C,(E,B,A)) is Element of K10( the carrier of E)

{ (b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

union C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,(union C),B) is Element of K10( the carrier of E)

{ (b

{ (E,b

union { (E,b

A is set

X is Element of the carrier of E

A is Element of the carrier of E

X + A is Element of the carrier of E

c is set

b is Element of K10( the carrier of E)

(E,b,B) is Element of K10( the carrier of E)

{ (b

X is set

A is Element of K10( the carrier of E)

(E,A,B) is Element of K10( the carrier of E)

{ (b

c is Element of the carrier of E

b is Element of the carrier of E

c + b is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

union C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,B,(union C)) is Element of K10( the carrier of E)

{ (b

{ (E,B,b

union { (E,B,b

{ (E,b

A is set

X is Element of K10( the carrier of E)

(E,X,B) is Element of K10( the carrier of E)

{ (b

(E,B,X) is Element of K10( the carrier of E)

{ (b

X is Element of K10( the carrier of E)

(E,B,X) is Element of K10( the carrier of E)

{ (b

(E,X,B) is Element of K10( the carrier of E)

{ (b

(E,(union C),B) is Element of K10( the carrier of E)

{ (b

union { (E,b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

meet C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,(meet C),B) is Element of K10( the carrier of E)

{ (b

{ (E,b

meet { (E,b

A is Element of K10( the carrier of E)

(E,A,B) is Element of K10( the carrier of E)

{ (b

A is set

X is Element of K10( the carrier of E)

(E,X,B) is Element of K10( the carrier of E)

{ (b

A is set

c is Element of the carrier of E

b is Element of the carrier of E

c + b is Element of the carrier of E

c is set

g is Element of K10( the carrier of E)

(E,g,B) is Element of K10( the carrier of E)

{ (b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

meet C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,B,(meet C)) is Element of K10( the carrier of E)

{ (b

{ (E,B,b

meet { (E,B,b

{ (E,b

A is set

X is Element of K10( the carrier of E)

(E,X,B) is Element of K10( the carrier of E)

{ (b

(E,B,X) is Element of K10( the carrier of E)

{ (b

X is Element of K10( the carrier of E)

(E,B,X) is Element of K10( the carrier of E)

{ (b

(E,X,B) is Element of K10( the carrier of E)

{ (b

meet { (E,b

E is non empty addLoopStr

the carrier of E is non empty set

K10( the carrier of E) is non empty set

B is Element of K10( the carrier of E)

A is Element of K10( the carrier of E)

C is Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (b

C + A is Element of K10( the carrier of E)

{ (b

X is set

A is Element of the carrier of E

c is Element of the carrier of E

A + c is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is Element of the carrier of E

B is non empty Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (C + b

A is non empty Element of K10( the carrier of E)

(E,(C + B),A) is Element of K10( the carrier of E)

{ (b

C + A is Element of K10( the carrier of E)

{ (C + b

(E,B,(C + A)) is Element of K10( the carrier of E)

{ (b

(E,B,A) is Element of K10( the carrier of E)

{ (b

C + (E,B,A) is Element of K10( the carrier of E)

{ (C + b

X is set

A is Element of the carrier of E

c is Element of the carrier of E

A + c is Element of the carrier of E

b is Element of the carrier of E

C + b is Element of the carrier of E

C + c is Element of the carrier of E

b + (C + c) is Element of the carrier of E

A is Element of the carrier of E

c is Element of the carrier of E

A + c is Element of the carrier of E

b is Element of the carrier of E

C + b is Element of the carrier of E

C + A is Element of the carrier of E

(C + A) + b is Element of the carrier of E

X is set

A is Element of the carrier of E

c is Element of the carrier of E

A + c is Element of the carrier of E

b is Element of the carrier of E

C + b is Element of the carrier of E

b + c is Element of the carrier of E

C + (b + c) is Element of the carrier of E

B + A is Element of K10( the carrier of E)

A is Element of the carrier of E

C + A is Element of the carrier of E

c is Element of the carrier of E

b is Element of the carrier of E

c + b is Element of the carrier of E

C + c is Element of the carrier of E

(C + c) + b is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

meet C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,(meet C),B) is Element of K10( the carrier of E)

{ b

( not b

{ (E,b

meet { (E,b

X is set

A is Element of K10( the carrier of E)

(E,A,B) is Element of K10( the carrier of E)

{ b

( not b

A is set

X is Element of K10( the carrier of E)

(E,X,B) is Element of K10( the carrier of E)

{ b

( not b

A is set

c is Element of the carrier of E

b is set

c is Element of K10( the carrier of E)

(E,c,B) is Element of K10( the carrier of E)

{ b

( not b

g is Element of the carrier of E

c - g is Element of the carrier of E

- g is Element of the carrier of E

c + (- g) is Element of the carrier of E

c is Element of K10( the carrier of E)

(E,c,B) is Element of K10( the carrier of E)

{ b

( not b

c is Element of the carrier of E

b is Element of the carrier of E

c - b is Element of the carrier of E

- b is Element of the carrier of E

c + (- b) is Element of the carrier of E

b is Element of the carrier of E

c - b is Element of the carrier of E

- b is Element of the carrier of E

c + (- b) is Element of the carrier of E

c is set

g is Element of K10( the carrier of E)

(E,g,B) is Element of K10( the carrier of E)

{ b

( not b

w is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

meet C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

{ (E,B,b

meet { (E,B,b

(E,B,(meet C)) is Element of K10( the carrier of E)

{ b

( not b

X is set

A is Element of K10( the carrier of E)

(E,B,A) is Element of K10( the carrier of E)

{ b

( not b

A is set

A is set

c is Element of K10( the carrier of E)

(E,B,c) is Element of K10( the carrier of E)

{ b

( not b

X is Element of K10( the carrier of E)

(E,B,X) is Element of K10( the carrier of E)

{ b

( not b

c is Element of the carrier of E

b is Element of the carrier of E

c - b is Element of the carrier of E

- b is Element of the carrier of E

c + (- b) is Element of the carrier of E

c is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

union C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

{ (E,b

union { (E,b

(E,(union C),B) is Element of K10( the carrier of E)

{ b

( not b

A is set

X is set

A is Element of K10( the carrier of E)

(E,A,B) is Element of K10( the carrier of E)

{ b

( not b

c is Element of the carrier of E

b is Element of the carrier of E

c - b is Element of the carrier of E

- b is Element of the carrier of E

c + (- b) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

C is Element of K10(K10( the carrier of E))

union C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,B,(union C)) is Element of K10( the carrier of E)

{ b

( not b

{ (E,B,b

meet { (E,B,b

A is set

X is Element of K10( the carrier of E)

(E,B,X) is Element of K10( the carrier of E)

{ b

( not b

A is set

c is Element of the carrier of E

b is set

c is Element of K10( the carrier of E)

(E,B,c) is Element of K10( the carrier of E)

{ b

( not b

g is Element of the carrier of E

c - g is Element of the carrier of E

- g is Element of the carrier of E

c + (- g) is Element of the carrier of E

c is Element of K10( the carrier of E)

(E,B,c) is Element of K10( the carrier of E)

{ b

( not b

c is Element of the carrier of E

b is Element of the carrier of E

c - b is Element of the carrier of E

- b is Element of the carrier of E

c + (- b) is Element of the carrier of E

c is set

g is Element of K10( the carrier of E)

(E,B,g) is Element of K10( the carrier of E)

{ b

( not b

w is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

A is non empty Element of K10( the carrier of E)

(E,C,A) is Element of K10( the carrier of E)

{ b

( not b

(E,B,A) is Element of K10( the carrier of E)

{ b

( not b

X is set

A is Element of the carrier of E

c is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

A is non empty Element of K10( the carrier of E)

(E,A,B) is Element of K10( the carrier of E)

{ b

( not b

(E,A,C) is Element of K10( the carrier of E)

{ b

( not b

X is set

A is Element of the carrier of E

c is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is Element of the carrier of E

B is non empty Element of K10( the carrier of E)

C + B is Element of K10( the carrier of E)

{ (C + b

A is non empty Element of K10( the carrier of E)

(E,(C + B),A) is Element of K10( the carrier of E)

{ b

( not b

C + A is Element of K10( the carrier of E)

{ (C + b

(E,B,(C + A)) is Element of K10( the carrier of E)

{ b

( not b

(E,B,A) is Element of K10( the carrier of E)

{ b

( not b

C + (E,B,A) is Element of K10( the carrier of E)

{ (C + b

X is set

A is Element of the carrier of E

c is Element of the carrier of E

b is Element of the carrier of E

C + b is Element of the carrier of E

A - b is Element of the carrier of E

- b is Element of the carrier of E

A + (- b) is Element of the carrier of E

c is Element of the carrier of E

C + c is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

(A - b) - C is Element of the carrier of E

- C is Element of the carrier of E

(A - b) + (- C) is Element of the carrier of E

A is Element of the carrier of E

c is Element of the carrier of E

C + c is Element of the carrier of E

A - (C + c) is Element of the carrier of E

- (C + c) is Element of the carrier of E

A + (- (C + c)) is Element of the carrier of E

C + (A - (C + c)) is Element of the carrier of E

C + A is Element of the carrier of E

(C + A) - (C + c) is Element of the carrier of E

(C + A) + (- (C + c)) is Element of the carrier of E

C - (C + c) is Element of the carrier of E

C + (- (C + c)) is Element of the carrier of E

A + (C - (C + c)) is Element of the carrier of E

C - C is Element of the carrier of E

C + (- C) is Element of the carrier of E

(C - C) - c is Element of the carrier of E

- c is Element of the carrier of E

(C - C) + (- c) is Element of the carrier of E

A + ((C - C) - c) is Element of the carrier of E

0. E is V52(E) Element of the carrier of E

(0. E) - c is Element of the carrier of E

(0. E) + (- c) is Element of the carrier of E

A + ((0. E) - c) is Element of the carrier of E

A - c is Element of the carrier of E

A + (- c) is Element of the carrier of E

X is set

A is Element of the carrier of E

c is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

b is Element of the carrier of E

C + b is Element of the carrier of E

A - C is Element of the carrier of E

- C is Element of the carrier of E

A + (- C) is Element of the carrier of E

(A - C) - c is Element of the carrier of E

(A - C) + (- c) is Element of the carrier of E

C + c is Element of the carrier of E

A - (C + c) is Element of the carrier of E

- (C + c) is Element of the carrier of E

A + (- (C + c)) is Element of the carrier of E

(C + b) - C is Element of the carrier of E

(C + b) + (- C) is Element of the carrier of E

C + (A - C) is Element of the carrier of E

A is Element of the carrier of E

C + A is Element of the carrier of E

b is Element of the carrier of E

c is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

(C + A) - c is Element of the carrier of E

(C + A) + (- c) is Element of the carrier of E

C + (A - c) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,C,B) is Element of K10( the carrier of E)

{ b

( not b

A is non empty Element of K10( the carrier of E)

(E,(E,C,B),A) is Element of K10( the carrier of E)

{ b

( not b

(E,B,A) is Element of K10( the carrier of E)

{ (b

(E,C,(E,B,A)) is Element of K10( the carrier of E)

{ b

( not b

X is set

A is Element of the carrier of E

c is Element of the carrier of E

b is Element of the carrier of E

c is Element of the carrier of E

b + c is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

g is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

g - b is Element of the carrier of E

- b is Element of the carrier of E

g + (- b) is Element of the carrier of E

A is Element of the carrier of E

c is Element of the carrier of E

b is Element of the carrier of E

b + c is Element of the carrier of E

A - (b + c) is Element of the carrier of E

- (b + c) is Element of the carrier of E

A + (- (b + c)) is Element of the carrier of E

A - c is Element of the carrier of E

- c is Element of the carrier of E

A + (- c) is Element of the carrier of E

(A - c) - b is Element of the carrier of E

- b is Element of the carrier of E

(A - c) + (- b) is Element of the carrier of E

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

C is Element of K10( the carrier of E)

B is set

A is Element of K10( the carrier of E)

(E,A,C) is Element of K10( the carrier of E)

{ (b

B is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

A is Element of K10( the carrier of E)

B . A is Element of bool the carrier of E

(E,A,C) is Element of K10( the carrier of E)

{ (b

X is Element of K10( the carrier of E)

(E,X,C) is Element of K10( the carrier of E)

{ (b

A is Element of K10( the carrier of E)

B . A is Element of bool the carrier of E

(E,A,C) is Element of K10( the carrier of E)

{ (b

B is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

A is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

X is set

B . X is set

A is Element of K10( the carrier of E)

(E,A,C) is Element of K10( the carrier of E)

{ (b

A . X is set

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

C is Element of K10( the carrier of E)

B is set

A is Element of K10( the carrier of E)

(E,A,C) is Element of K10( the carrier of E)

{ b

( not b

B is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

A is Element of K10( the carrier of E)

B . A is Element of bool the carrier of E

(E,A,C) is Element of K10( the carrier of E)

{ b

( not b

X is Element of K10( the carrier of E)

(E,X,C) is Element of K10( the carrier of E)

{ b

( not b

A is Element of K10( the carrier of E)

B . A is Element of bool the carrier of E

(E,A,C) is Element of K10( the carrier of E)

{ b

( not b

B is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

A is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

X is set

B . X is set

A is Element of K10( the carrier of E)

(E,A,C) is Element of K10( the carrier of E)

{ b

( not b

A . X is set

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

C is Element of K10(K10( the carrier of E))

union C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,B) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

(E,B) . (union C) is Element of bool the carrier of E

{ ((E,B) . b

union { ((E,B) . b

{ (E,b

A is set

X is Element of K10( the carrier of E)

(E,X,B) is Element of K10( the carrier of E)

{ (b

(E,B) . X is Element of bool the carrier of E

X is Element of K10( the carrier of E)

(E,B) . X is Element of bool the carrier of E

(E,X,B) is Element of K10( the carrier of E)

{ (b

(E,(union C),B) is Element of K10( the carrier of E)

{ (b

union { (E,b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

A is non empty Element of K10( the carrier of E)

(E,A) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

(E,A) . C is Element of bool the carrier of E

(E,A) . B is Element of bool the carrier of E

A + C is Element of K10( the carrier of E)

{ (b

A + B is Element of K10( the carrier of E)

{ (b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

C is Element of the carrier of E

B is non empty Element of K10( the carrier of E)

(E,B) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

A is non empty Element of K10( the carrier of E)

C + A is Element of K10( the carrier of E)

{ (C + b

(E,B) . (C + A) is Element of bool the carrier of E

(E,B) . A is Element of bool the carrier of E

C + ((E,B) . A) is Element of K10( the carrier of E)

{ (C + b

(E,(C + A),B) is Element of K10( the carrier of E)

{ (b

(E,A,B) is Element of K10( the carrier of E)

{ (b

C + (E,A,B) is Element of K10( the carrier of E)

{ (C + b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

K10(K10( the carrier of E)) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

C is Element of K10(K10( the carrier of E))

meet C is Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

(E,B) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

(E,B) . (meet C) is Element of bool the carrier of E

{ ((E,B) . b

meet { ((E,B) . b

{ (E,b

A is set

X is Element of K10( the carrier of E)

(E,X,B) is Element of K10( the carrier of E)

{ b

( not b

(E,B) . X is Element of bool the carrier of E

X is Element of K10( the carrier of E)

(E,B) . X is Element of bool the carrier of E

(E,X,B) is Element of K10( the carrier of E)

{ b

( not b

(E,(meet C),B) is Element of K10( the carrier of E)

{ b

( not b

meet { (E,b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

C is non empty Element of K10( the carrier of E)

B is non empty Element of K10( the carrier of E)

A is non empty Element of K10( the carrier of E)

(E,A) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

(E,A) . C is Element of bool the carrier of E

(E,A) . B is Element of bool the carrier of E

(E,C,A) is Element of K10( the carrier of E)

{ b

( not b

(E,B,A) is Element of K10( the carrier of E)

{ b

( not b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

C is Element of the carrier of E

B is non empty Element of K10( the carrier of E)

(E,B) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

A is non empty Element of K10( the carrier of E)

C + A is Element of K10( the carrier of E)

{ (C + b

(E,B) . (C + A) is Element of bool the carrier of E

(E,B) . A is Element of bool the carrier of E

C + ((E,B) . A) is Element of K10( the carrier of E)

{ (C + b

(E,(C + A),B) is Element of K10( the carrier of E)

{ b

( not b

(E,A,B) is Element of K10( the carrier of E)

{ b

( not b

C + (E,A,B) is Element of K10( the carrier of E)

{ (C + b

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

C is non empty Element of K10( the carrier of E)

(E,C) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

(E,C) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

B is non empty Element of K10( the carrier of E)

the carrier of E \ B is Element of K10( the carrier of E)

(E,C) . ( the carrier of E \ B) is Element of bool the carrier of E

(E,C) . B is Element of bool the carrier of E

the carrier of E \ ((E,C) . B) is Element of K10( the carrier of E)

(E,C) . ( the carrier of E \ B) is Element of bool the carrier of E

(E,C) . B is Element of bool the carrier of E

the carrier of E \ ((E,C) . B) is Element of K10( the carrier of E)

(E,( the carrier of E \ B),C) is Element of K10( the carrier of E)

{ (b

(E,B,C) is Element of K10( the carrier of E)

{ b

( not b

the carrier of E \ (E,B,C) is Element of K10( the carrier of E)

(E,( the carrier of E \ B),C) is Element of K10( the carrier of E)

{ b

( not b

(E,B,C) is Element of K10( the carrier of E)

{ (b

the carrier of E \ (E,B,C) is Element of K10( the carrier of E)

E is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V103() RLSStruct

the carrier of E is non empty set

K10( the carrier of E) is non empty set

bool the carrier of E is non empty Element of K10(K10( the carrier of E))

K10(K10( the carrier of E)) is non empty set

C is non empty Element of K10( the carrier of E)

(E,C) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

K11((bool the carrier of E),(bool the carrier of E)) is non empty set

K10(K11((bool the carrier of E),(bool the carrier of E))) is non empty set

(E,C) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

B is non empty Element of K10( the carrier of E)

(E,B) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

(E,C) . B is Element of bool the carrier of E

(E,((E,C) . B)) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

(E,B) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

(E,((E,C) . B)) is V16() V19( bool the carrier of E) V20( bool the carrier of E) Function-like V30( bool the carrier of E, bool the carrier of E) Element of K10(K11((bool the carrier of E),(bool the carrier of E)))

A is non empty Element of K10( the carrier of E)

(E,B) . A is Element of bool the carrier of E

(E,C) . ((E,B) . A) is Element of bool the carrier of E

(E,((E,C) . B)) . A is Element of bool the carrier of E

(E,B) . A is Element of bool the carrier of E

(E,C) . ((E,B) . A) is Element of bool the carrier of E

(E,((E,C) . B)) . A is Element of bool the carrier of E

(E,A,B) is Element of K10( the carrier of E)

{ (b

(E,C) . (E,A,B) is Element of bool the carrier of E

(E,(E,A,B),C) is Element of K10( the carrier of E)

{ (b

(E,B,C) is Element of K10( the carrier of E)

{ (b

(E,A,(E,B,C)) is Element of K10( the carrier of E)

{ (b

(E,A,((E,C) . B)) is Element of K10( the carrier of E)

{ (b

(E,A,B) is Element of K10( the carrier of E)

{ b

( not b

(E,C) . (E,A,B) is Element of bool the carrier of E

(E,(E,A,B),C) is Element of K10( the carrier of E)

{ b

( not b

(E,A,(E,B,C)) is Element of K10( the carrier of E)

{ b

( not b

(E,A,((E,C) . B)) is Element of K10( the carrier of E)

{ b

( not b