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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in C ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
B + C is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in C ) } is set
(E,C,B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in C ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in B ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
B + C is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in C ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in B ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
{ (b1 + C) where b1 is Element of the carrier of E : b1 in B } is set
union { (b1 + C) where b1 is Element of the carrier of E : b1 in B } is set
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 + b1) where b1 is Element of the carrier of E : b1 in C } is set
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 + b1) where b1 is Element of the carrier of E : b1 in C } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in C ) } is set
{ (b1 + C) where b1 is Element of the carrier of E : b1 in B } is set
meet { (b1 + C) where b1 is Element of the carrier of E : b1 in B } is set
A is set
X is Element of the carrier of E
X + C is Element of K10( the carrier of E)
{ (X + b1) where b1 is Element of the carrier of E : b1 in C } is set
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 + b1) where b1 is Element of the carrier of E : b1 in C } is set
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 + b1) where b1 is Element of the carrier of E : b1 in C } is set
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 + b1) where b1 is Element of the carrier of E : b1 in C } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
(- 1) (.) B is Element of K10( the carrier of E)
{ ((- 1) * b1) where b1 is Element of the carrier of E : b1 in B } is set
{ b1 where b1 is Element of the carrier of E : not (b1 + ((- 1) (.) B)) /\ C = {} } is set
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 + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
(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 + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
(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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in C ) } is set
(- 1) (.) B is Element of K10( the carrier of E)
{ ((- 1) * b1) where b1 is Element of the carrier of E : b1 in B } is set
{ b1 where b1 is Element of the carrier of E : b1 + ((- 1) (.) B) c= C } is set
A is set
X is Element of the carrier of E
X + ((- 1) (.) B) is Element of K10( the carrier of E)
{ (X + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
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 + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in the carrier of E \ C & b2 in B ) } is set
(E,C,B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in C ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in the carrier of E \ C ) } is set
C + B is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in B ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in A ) } is set
(- 1) (.) B is Element of K10( the carrier of E)
{ ((- 1) * b1) where b1 is Element of the carrier of E : b1 in B } is set
{ b1 where b1 is Element of the carrier of E : not (b1 + ((- 1) (.) B)) /\ ( the carrier of E \ C) = {} } is set
{ b1 where b1 is Element of the carrier of E : b1 + ((- 1) (.) B) c= C } is set
A is set
X is Element of the carrier of E
X + ((- 1) (.) B) is Element of K10( the carrier of E)
{ (X + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
(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 + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
X is Element of the carrier of E
X + ((- 1) (.) B) is Element of K10( the carrier of E)
{ (X + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
(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)
{ b1 where b1 is Element of the carrier of E : b1 + ((- 1) (.) B) c= the carrier of E \ C } is set
{ b1 where b1 is Element of the carrier of E : not (b1 + ((- 1) (.) B)) /\ C = {} } is set
A is set
X is Element of the carrier of E
X + ((- 1) (.) B) is Element of K10( the carrier of E)
{ (X + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
A is Element of the carrier of E
A + ((- 1) (.) B) is Element of K10( the carrier of E)
{ (A + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
(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 + b1) where b1 is Element of the carrier of E : b1 in (- 1) (.) B } is set
(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 \ { b1 where b1 is Element of the carrier of E : b1 + ((- 1) (.) B) c= C } is Element of K10( the carrier of E)
the carrier of E \ { b1 where b1 is Element of the carrier of E : not (b1 + ((- 1) (.) 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
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
B + C is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in C ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in X ) } is set
X + A is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in A ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
A is Element of K10( the carrier of E)
(C + B) + A is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C + B & b2 in A ) } is set
B + A is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in A ) } is set
C + (B + A) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B + A ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
A is non empty Element of K10( the carrier of E)
(E,(E,C,B),A) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in (E,C,B) & b2 in A ) } is set
(E,B,A) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in A ) } is set
(E,C,(E,B,A)) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in (E,B,A) ) } 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
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in union C & b2 in B ) } is set
{ (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
union { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in b & b2 in B ) } 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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in B ) } 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
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in union C ) } is set
{ (E,B,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
union { (E,B,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
{ (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
A is set
X is Element of K10( the carrier of E)
(E,X,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in B ) } is set
(E,B,X) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in X ) } is set
X is Element of K10( the carrier of E)
(E,B,X) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in X ) } is set
(E,X,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in B ) } is set
(E,(union C),B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in union C & b2 in B ) } is set
union { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } 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
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in meet C & b2 in B ) } is set
{ (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
meet { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
A is Element of K10( the carrier of E)
(E,A,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in B ) } is set
A is set
X is Element of K10( the carrier of E)
(E,X,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in B ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in g & b2 in B ) } 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
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in meet C ) } is set
{ (E,B,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
meet { (E,B,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
{ (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
A is set
X is Element of K10( the carrier of E)
(E,X,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in B ) } is set
(E,B,X) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in X ) } is set
X is Element of K10( the carrier of E)
(E,B,X) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in X ) } is set
(E,X,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in B ) } is set
meet { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in B ) } is set
C + A is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C & b2 in A ) } is set
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 + b1) where b1 is Element of the carrier of E : b1 in B } is set
A is non empty Element of K10( the carrier of E)
(E,(C + B),A) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C + B & b2 in A ) } is set
C + A is Element of K10( the carrier of E)
{ (C + b1) where b1 is Element of the carrier of E : b1 in A } is set
(E,B,(C + A)) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in C + A ) } is set
(E,B,A) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in A ) } is set
C + (E,B,A) is Element of K10( the carrier of E)
{ (C + b1) where b1 is Element of the carrier of E : b1 in (E,B,A) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in meet C ) } is set
{ (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
meet { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } 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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in A ) } is set
A is set
X is Element of K10( the carrier of E)
(E,X,B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in X ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in c ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in c ) } 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
- 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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in g ) } is set
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,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
meet { (E,B,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
(E,B,(meet C)) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in meet C or b1 - b2 in B ) } is set
X is set
A is Element of K10( the carrier of E)
(E,B,A) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in B ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in c or b1 - b2 in B ) } is set
X is Element of K10( the carrier of E)
(E,B,X) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in X or b1 - b2 in B ) } 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
- 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,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
union { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
(E,(union C),B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in union C ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in 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
- 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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in union C or b1 - b2 in B ) } is set
{ (E,B,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
meet { (E,B,b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
A is set
X is Element of K10( the carrier of E)
(E,B,X) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in X or b1 - b2 in B ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in c or b1 - b2 in B ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in c or b1 - b2 in B ) } 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
- 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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in g or b1 - b2 in B ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in C ) } is set
(E,B,A) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in B ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in A ) } is set
(E,A,C) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in A ) } is set
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 + b1) where b1 is Element of the carrier of E : b1 in B } is set
A is non empty Element of K10( the carrier of E)
(E,(C + B),A) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in C + B ) } is set
C + A is Element of K10( the carrier of E)
{ (C + b1) where b1 is Element of the carrier of E : b1 in A } is set
(E,B,(C + A)) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C + A or b1 - b2 in B ) } is set
(E,B,A) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in B ) } is set
C + (E,B,A) is Element of K10( the carrier of E)
{ (C + b1) where b1 is Element of the carrier of E : b1 in (E,B,A) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in C ) } is set
A is non empty Element of K10( the carrier of E)
(E,(E,C,B),A) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in (E,C,B) ) } is set
(E,B,A) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in A ) } is set
(E,C,(E,B,A)) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in (E,B,A) or b1 - b2 in C ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in C ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in C ) } is set
X is Element of K10( the carrier of E)
(E,X,C) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in C ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in C ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in C ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in A ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in A ) } is set
X is Element of K10( the carrier of E)
(E,X,C) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in X ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in A ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in A ) } is set
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) . b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
union { ((E,B) . b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
{ (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
A is set
X is Element of K10( the carrier of E)
(E,X,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in B ) } is set
(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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in X & b2 in B ) } is set
(E,(union C),B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in union C & b2 in B ) } is set
union { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } 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
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in C ) } is set
A + B is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in B ) } 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
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 + b1) where b1 is Element of the carrier of E : b1 in A } is set
(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 + b1) where b1 is Element of the carrier of E : b1 in (E,B) . A } is set
(E,(C + A),B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in C + A & b2 in B ) } is set
(E,A,B) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in B ) } is set
C + (E,A,B) is Element of K10( the carrier of E)
{ (C + b1) where b1 is Element of the carrier of E : b1 in (E,A,B) } 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))
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) . b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
meet { ((E,B) . b1) where b1 is Element of K10( the carrier of E) : b1 in C } is set
{ (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } is set
A is set
X is Element of K10( the carrier of E)
(E,X,B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in X ) } is set
(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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in X ) } is set
(E,(meet C),B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in meet C ) } is set
meet { (E,b1,B) where b1 is Element of K10( the carrier of E) : b1 in C } 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
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in C ) } is set
(E,B,A) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in A or b1 - b2 in B ) } 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
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 + b1) where b1 is Element of the carrier of E : b1 in A } is set
(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 + b1) where b1 is Element of the carrier of E : b1 in (E,B) . A } is set
(E,(C + A),B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in C + A ) } is set
(E,A,B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in A ) } is set
C + (E,A,B) is Element of K10( the carrier of E)
{ (C + b1) where b1 is Element of the carrier of E : b1 in (E,A,B) } 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
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in the carrier of E \ B & b2 in C ) } is set
(E,B,C) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in B ) } is set
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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in the carrier of E \ B ) } is set
(E,B,C) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in C ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in B ) } is set
(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)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in (E,A,B) & b2 in C ) } is set
(E,B,C) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in B & b2 in C ) } is set
(E,A,(E,B,C)) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in (E,B,C) ) } is set
(E,A,((E,C) . B)) is Element of K10( the carrier of E)
{ (b1 + b2) where b1, b2 is Element of the carrier of E : ( b1 in A & b2 in (E,C) . B ) } is set
(E,A,B) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in B or b1 - b2 in A ) } is set
(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)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in C or b1 - b2 in (E,A,B) ) } is set
(E,A,(E,B,C)) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in (E,B,C) or b1 - b2 in A ) } is set
(E,A,((E,C) . B)) is Element of K10( the carrier of E)
{ b1 where b1 is Element of the carrier of E : for b2 being Element of the carrier of E holds
( not b2 in (E,C) . B or b1 - b2 in A ) } is set