:: ANALMETR semantic presentation

REAL is V29() V30() V31() V35() set
NAT is V29() V30() V31() V32() V33() V34() V35() Element of bool REAL
bool REAL is non empty set
NAT is V29() V30() V31() V32() V33() V34() V35() set
bool NAT is non empty set
bool NAT is non empty set
{} is empty V29() V30() V31() V32() V33() V34() V35() set
1 is non empty V17() V18() V19() V26() V27() V28() V29() V30() V31() V32() V33() V34() Element of NAT
0 is empty V17() V18() V19() V26() V27() V28() V29() V30() V31() V32() V33() V34() V35() Element of NAT
- 1 is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
w0 + w0 is Element of the carrier of V0
w0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,w0,(- w0)) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * y0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * V0 is Element of the carrier of V0
(y0 * y0) + (POS * V0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
y0 + K is V17() V27() V28() Element of REAL
(y0 + K) * y0 is Element of the carrier of V0
y0 - K is V17() V27() V28() Element of REAL
(y0 - K) * y0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * V0 is Element of the carrier of V0
(K * y0) + (a * V0) is Element of the carrier of V0
POS + a is V17() V27() V28() Element of REAL
(POS + a) * V0 is Element of the carrier of V0
((y0 + K) * y0) + ((POS + a) * V0) is Element of the carrier of V0
POS - a is V17() V27() V28() Element of REAL
(POS - a) * V0 is Element of the carrier of V0
((y0 - K) * y0) + ((POS - a) * V0) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + (K * y0) is Element of the carrier of V0
(((y0 * y0) + (POS * V0)) + (K * y0)) + (a * V0) is Element of the carrier of V0
(y0 * y0) + (K * y0) is Element of the carrier of V0
((y0 * y0) + (K * y0)) + (POS * V0) is Element of the carrier of V0
(((y0 * y0) + (K * y0)) + (POS * V0)) + (a * V0) is Element of the carrier of V0
((y0 + K) * y0) + (POS * V0) is Element of the carrier of V0
(((y0 + K) * y0) + (POS * V0)) + (a * V0) is Element of the carrier of V0
(POS * V0) + (a * V0) is Element of the carrier of V0
((y0 + K) * y0) + ((POS * V0) + (a * V0)) is Element of the carrier of V0
- (K * y0) is Element of the carrier of V0
- (a * V0) is Element of the carrier of V0
(- (K * y0)) + (- (a * V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((- (K * y0)) + (- (a * V0))) is Element of the carrier of V0
- y0 is Element of the carrier of V0
K * (- y0) is Element of the carrier of V0
(K * (- y0)) + (- (a * V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((K * (- y0)) + (- (a * V0))) is Element of the carrier of V0
- V0 is Element of the carrier of V0
a * (- V0) is Element of the carrier of V0
(K * (- y0)) + (a * (- V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((K * (- y0)) + (a * (- V0))) is Element of the carrier of V0
- K is V17() V27() V28() Element of REAL
(- K) * y0 is Element of the carrier of V0
((- K) * y0) + (a * (- V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + (((- K) * y0) + (a * (- V0))) is Element of the carrier of V0
- a is V17() V27() V28() Element of REAL
(- a) * V0 is Element of the carrier of V0
((- K) * y0) + ((- a) * V0) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + (((- K) * y0) + ((- a) * V0)) is Element of the carrier of V0
((y0 * y0) + (POS * V0)) + ((- K) * y0) is Element of the carrier of V0
(((y0 * y0) + (POS * V0)) + ((- K) * y0)) + ((- a) * V0) is Element of the carrier of V0
(y0 * y0) + ((- K) * y0) is Element of the carrier of V0
((y0 * y0) + ((- K) * y0)) + (POS * V0) is Element of the carrier of V0
(((y0 * y0) + ((- K) * y0)) + (POS * V0)) + ((- a) * V0) is Element of the carrier of V0
y0 + (- K) is V17() V27() V28() Element of REAL
(y0 + (- K)) * y0 is Element of the carrier of V0
((y0 + (- K)) * y0) + (POS * V0) is Element of the carrier of V0
(((y0 + (- K)) * y0) + (POS * V0)) + ((- a) * V0) is Element of the carrier of V0
(POS * V0) + ((- a) * V0) is Element of the carrier of V0
((y0 + (- K)) * y0) + ((POS * V0) + ((- a) * V0)) is Element of the carrier of V0
POS + (- a) is V17() V27() V28() Element of REAL
(POS + (- a)) * V0 is Element of the carrier of V0
((y0 - K) * y0) + ((POS + (- a)) * V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(0 * w0) + (0 * y0) is Element of the carrier of V0
(0. V0) + (0 * y0) is Element of the carrier of V0
(0. V0) + (0. V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * y0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
(w0 * y0) + (y0 * V0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
POS * w0 is V17() V27() V28() Element of REAL
(POS * w0) * y0 is Element of the carrier of V0
POS * y0 is V17() V27() V28() Element of REAL
(POS * y0) * V0 is Element of the carrier of V0
((POS * w0) * y0) + ((POS * y0) * V0) is Element of the carrier of V0
POS * (w0 * y0) is Element of the carrier of V0
POS * (y0 * V0) is Element of the carrier of V0
(POS * (w0 * y0)) + (POS * (y0 * V0)) is Element of the carrier of V0
((POS * w0) * y0) + (POS * (y0 * V0)) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is V17() V27() V28() Element of REAL
V0 * w0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * y0 is Element of the carrier of V0
(V0 * w0) + (w0 * y0) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
(y0 * w0) + (POS * y0) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
((V0 * w0) + (w0 * y0)) - ((y0 * w0) + (POS * y0)) is Element of the carrier of V0
- ((y0 * w0) + (POS * y0)) is Element of the carrier of V0
K176(V0,((V0 * w0) + (w0 * y0)),(- ((y0 * w0) + (POS * y0)))) is Element of the carrier of V0
V0 - y0 is V17() V27() V28() Element of REAL
(V0 - y0) * w0 is Element of the carrier of V0
w0 - POS is V17() V27() V28() Element of REAL
(w0 - POS) * y0 is Element of the carrier of V0
((V0 - y0) * w0) + ((w0 - POS) * y0) is Element of the carrier of V0
- y0 is V17() V27() V28() Element of REAL
(- y0) + V0 is V17() V27() V28() Element of REAL
- POS is V17() V27() V28() Element of REAL
(- POS) + w0 is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
(y0 * V0) + (POS * w0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
p is V17() V27() V28() Element of REAL
p * V0 is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
(p * V0) + (q * w0) is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * V0 is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * w0 is Element of the carrier of V0
(x * V0) + (c₁₃ * w0) is Element of the carrier of V0
p * x is V17() V27() V28() Element of REAL
q * c₁₃ is V17() V27() V28() Element of REAL
(p * x) + (q * c₁₃) is V17() V27() V28() Element of REAL
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
(y0 * V0) + (POS * w0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
(1 * w0) + (0. V0) is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(1 * w0) + (0 * y0) is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
(0. V0) + (1 * y0) is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (1 * y0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
(0. V0) + y0 is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
(0. V0) + (1 * y0) is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (1 * y0) is Element of the carrier of V0
1 * 0 is V17() V27() V28() Element of REAL
0 * 1 is V17() V27() V28() Element of REAL
(1 * 0) + (0 * 1) is V17() V27() V28() Element of REAL
w0 + (0. V0) is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
(1 * w0) + (0. V0) is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(1 * w0) + (0 * y0) is Element of the carrier of V0
V0 is non empty V78() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * V0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
(y0 * V0) + (POS * w0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
(y0 * w0) + (POS * y0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * w0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * y0 is Element of the carrier of V0
(K * w0) + (a * y0) is Element of the carrier of V0
(0. V0) + (0. V0) is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (0. V0) is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
(0 * w0) + (0 * y0) is Element of the carrier of V0
y0 * 0 is V17() V27() V28() Element of REAL
POS * 0 is V17() V27() V28() Element of REAL
(y0 * 0) + (POS * 0) is V17() V27() V28() Element of REAL
0 * K is V17() V27() V28() Element of REAL
0 * a is V17() V27() V28() Element of REAL
(0 * K) + (0 * a) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
(K * V0) + (a * w0) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * V0 is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
(p * V0) + (q * w0) is Element of the carrier of V0
K * p is V17() V27() V28() Element of REAL
a * q is V17() V27() V28() Element of REAL
(K * p) + (a * q) is V17() V27() V28() Element of REAL
POS * (p * V0) is Element of the carrier of V0
POS * (q * w0) is Element of the carrier of V0
(POS * (p * V0)) + (POS * (q * w0)) is Element of the carrier of V0
POS * p is V17() V27() V28() Element of REAL
(POS * p) * V0 is Element of the carrier of V0
((POS * p) * V0) + (POS * (q * w0)) is Element of the carrier of V0
POS * q is V17() V27() V28() Element of REAL
(POS * q) * w0 is Element of the carrier of V0
((POS * p) * V0) + ((POS * q) * w0) is Element of the carrier of V0
y0 * K is V17() V27() V28() Element of REAL
(y0 * K) * (POS * p) is V17() V27() V28() Element of REAL
y0 * a is V17() V27() V28() Element of REAL
(y0 * a) * (POS * q) is V17() V27() V28() Element of REAL
((y0 * K) * (POS * p)) + ((y0 * a) * (POS * q)) is V17() V27() V28() Element of REAL
POS * y0 is V17() V27() V28() Element of REAL
(POS * y0) * ((K * p) + (a * q)) is V17() V27() V28() Element of REAL
y0 * (K * V0) is Element of the carrier of V0
y0 * (a * w0) is Element of the carrier of V0
(y0 * (K * V0)) + (y0 * (a * w0)) is Element of the carrier of V0
(y0 * K) * V0 is Element of the carrier of V0
((y0 * K) * V0) + (y0 * (a * w0)) is Element of the carrier of V0
(y0 * a) * w0 is Element of the carrier of V0
((y0 * K) * V0) + ((y0 * a) * w0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * y0 is Element of the carrier of V0
(w0 * w0) + (y0 * y0) is Element of the carrier of V0
y0 * w0 is Element of the carrier of V0
- w0 is V17() V27() V28() Element of REAL
(- w0) * y0 is Element of the carrier of V0
(y0 * w0) + ((- w0) * y0) is Element of the carrier of V0
w0 * y0 is V17() V27() V28() Element of REAL
y0 * (- w0) is V17() V27() V28() Element of REAL
(w0 * y0) + (y0 * (- w0)) is V17() V27() V28() Element of REAL
K is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
(0 * w0) + (0. V0) is Element of the carrier of V0
POS is Element of the carrier of V0
POS is Element of the carrier of V0
K is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(a * w0) + (p * y0) is Element of the carrier of V0
POS * a is V17() V27() V28() Element of REAL
K * p is V17() V27() V28() Element of REAL
(POS * a) + (K * p) is V17() V27() V28() Element of REAL
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * y0 is Element of the carrier of V0
(q * w0) + (x * y0) is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * w0 is Element of the carrier of V0
c9 is V17() V27() V28() Element of REAL
c9 * y0 is Element of the carrier of V0
(c₁₃ * w0) + (c9 * y0) is Element of the carrier of V0
q * c₁₃ is V17() V27() V28() Element of REAL
x * c9 is V17() V27() V28() Element of REAL
(q * c₁₃) + (x * c9) is V17() V27() V28() Element of REAL
(c₁₃ * w0) + (0. V0) is Element of the carrier of V0
(a * w0) + (0. V0) is Element of the carrier of V0
1 * w0 is Element of the carrier of V0
0 * w0 is Element of the carrier of V0
0 * y0 is Element of the carrier of V0
c₁₃ * w0 is Element of the carrier of V0
c₁₃ * (a * w0) is Element of the carrier of V0
a * c₁₃ is V17() V27() V28() Element of REAL
(a * c₁₃) * w0 is Element of the carrier of V0
a * y0 is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
- K is V17() V27() V28() Element of REAL
(- K) * p is V17() V27() V28() Element of REAL
POS " is V17() V27() V28() Element of REAL
((- K) * p) * (POS ") is V17() V27() V28() Element of REAL
c9 * (((- K) * p) * (POS ")) is V17() V27() V28() Element of REAL
(- K) * c9 is V17() V27() V28() Element of REAL
((- K) * c9) * (POS ") is V17() V27() V28() Element of REAL
p * (((- K) * c9) * (POS ")) is V17() V27() V28() Element of REAL
1 * a is V17() V27() V28() Element of REAL
POS * (POS ") is V17() V27() V28() Element of REAL
(POS * (POS ")) * a is V17() V27() V28() Element of REAL
(POS * a) * (POS ") is V17() V27() V28() Element of REAL
1 * c₁₃ is V17() V27() V28() Element of REAL
(POS * (POS ")) * c₁₃ is V17() V27() V28() Element of REAL
POS * c₁₃ is V17() V27() V28() Element of REAL
(POS * c₁₃) * (POS ") is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(p * (((- K) * c9) * (POS "))) * w0 is Element of the carrier of V0
p * c9 is V17() V27() V28() Element of REAL
(p * c9) * y0 is Element of the carrier of V0
((p * (((- K) * c9) * (POS "))) * w0) + ((p * c9) * y0) is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
1 * y0 is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
N is V17() V27() V28() Element of REAL
N * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * w0 is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * y0 is Element of the carrier of V0
N is V17() V27() V28() Element of REAL
N * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 + y0 is Element of the carrier of V0
w0 - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,w0,(- y0)) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(a * w0) + (p * y0) is Element of the carrier of V0
POS * a is V17() V27() V28() Element of REAL
K * p is V17() V27() V28() Element of REAL
(POS * a) + (K * p) is V17() V27() V28() Element of REAL
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * y0 is Element of the carrier of V0
(q * w0) + (x * y0) is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * w0 is Element of the carrier of V0
c9 is V17() V27() V28() Element of REAL
c9 * y0 is Element of the carrier of V0
(c₁₃ * w0) + (c9 * y0) is Element of the carrier of V0
q * c₁₃ is V17() V27() V28() Element of REAL
x * c9 is V17() V27() V28() Element of REAL
(q * c₁₃) + (x * c9) is V17() V27() V28() Element of REAL
a + c₁₃ is V17() V27() V28() Element of REAL
POS * (a + c₁₃) is V17() V27() V28() Element of REAL
p + c9 is V17() V27() V28() Element of REAL
K * (p + c9) is V17() V27() V28() Element of REAL
(POS * (a + c₁₃)) + (K * (p + c9)) is V17() V27() V28() Element of REAL
a - c₁₃ is V17() V27() V28() Element of REAL
POS * (a - c₁₃) is V17() V27() V28() Element of REAL
p - c9 is V17() V27() V28() Element of REAL
K * (p - c9) is V17() V27() V28() Element of REAL
(POS * (a - c₁₃)) + (K * (p - c9)) is V17() V27() V28() Element of REAL
(a + c₁₃) * w0 is Element of the carrier of V0
(p + c9) * y0 is Element of the carrier of V0
((a + c₁₃) * w0) + ((p + c9) * y0) is Element of the carrier of V0
(a - c₁₃) * w0 is Element of the carrier of V0
(p - c9) * y0 is Element of the carrier of V0
((a - c₁₃) * w0) + ((p - c9) * y0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * w0 is V17() V27() V28() Element of REAL
w0 is V17() V27() V28() Element of REAL
w0 * w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * y0 is Element of the carrier of V0
(w0 * w0) + (y0 * y0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
w0 * POS is V17() V27() V28() Element of REAL
y0 * K is V17() V27() V28() Element of REAL
(w0 * POS) + (y0 * K) is V17() V27() V28() Element of REAL
y0 * y0 is V17() V27() V28() Element of REAL
w0 * w0 is V17() V27() V28() Element of REAL
0 * w0 is Element of the carrier of V0
(0 * w0) + (0. V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
V0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,V0,(- w0)) is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,w0,(- y0)) is Element of the carrier of V0
y0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,y0,(- V0)) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * w0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * y0 is Element of the carrier of V0
(POS * w0) + (K * y0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(a * w0) + (p * y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * w0 is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * y0 is Element of the carrier of V0
(q * w0) + (x * y0) is Element of the carrier of V0
POS - q is V17() V27() V28() Element of REAL
(POS - q) * w0 is Element of the carrier of V0
K - x is V17() V27() V28() Element of REAL
(K - x) * y0 is Element of the carrier of V0
((POS - q) * w0) + ((K - x) * y0) is Element of the carrier of V0
a - POS is V17() V27() V28() Element of REAL
(a - POS) * w0 is Element of the carrier of V0
p - K is V17() V27() V28() Element of REAL
(p - K) * y0 is Element of the carrier of V0
((a - POS) * w0) + ((p - K) * y0) is Element of the carrier of V0
q * (a - POS) is V17() V27() V28() Element of REAL
x * (p - K) is V17() V27() V28() Element of REAL
(q * (a - POS)) + (x * (p - K)) is V17() V27() V28() Element of REAL
q - a is V17() V27() V28() Element of REAL
(q - a) * w0 is Element of the carrier of V0
x - p is V17() V27() V28() Element of REAL
(x - p) * y0 is Element of the carrier of V0
((q - a) * w0) + ((x - p) * y0) is Element of the carrier of V0
POS * (q - a) is V17() V27() V28() Element of REAL
K * (x - p) is V17() V27() V28() Element of REAL
(POS * (q - a)) + (K * (x - p)) is V17() V27() V28() Element of REAL
a * (POS - q) is V17() V27() V28() Element of REAL
p * (K - x) is V17() V27() V28() Element of REAL
(a * (POS - q)) + (p * (K - x)) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * w0 is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * y0 is Element of the carrier of V0
(y0 * w0) + (POS * y0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * w0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * y0 is Element of the carrier of V0
(K * w0) + (a * y0) is Element of the carrier of V0
K * y0 is V17() V27() V28() Element of REAL
a * POS is V17() V27() V28() Element of REAL
(K * y0) + (a * POS) is V17() V27() V28() Element of REAL
y0 * y0 is V17() V27() V28() Element of REAL
POS * POS is V17() V27() V28() Element of REAL
(y0 * y0) + (POS * POS) is V17() V27() V28() Element of REAL
((y0 * y0) + (POS * POS)) " is V17() V27() V28() Element of REAL
((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ") is V17() V27() V28() Element of REAL
(((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0 is Element of the carrier of V0
(((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0 is V17() V27() V28() Element of REAL
((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) * w0 is Element of the carrier of V0
(((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS is V17() V27() V28() Element of REAL
((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) * y0 is Element of the carrier of V0
(((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) * w0) + (((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) * y0) is Element of the carrier of V0
w0 - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0) is Element of the carrier of V0
- ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0) is Element of the carrier of V0
K176(V0,w0,(- ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * V0))) is Element of the carrier of V0
K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) is V17() V27() V28() Element of REAL
(K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * w0 is Element of the carrier of V0
a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) is V17() V27() V28() Element of REAL
(a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * y0 is Element of the carrier of V0
((K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * w0) + ((a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * y0) is Element of the carrier of V0
(K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * y0 is V17() V27() V28() Element of REAL
(a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * POS is V17() V27() V28() Element of REAL
((K - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) * y0) + ((a - ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) * POS) is V17() V27() V28() Element of REAL
y0 * K is V17() V27() V28() Element of REAL
POS * a is V17() V27() V28() Element of REAL
(y0 * K) + (POS * a) is V17() V27() V28() Element of REAL
y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0) is V17() V27() V28() Element of REAL
POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS) is V17() V27() V28() Element of REAL
(y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) + (POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)) is V17() V27() V28() Element of REAL
(- 1) * ((y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) + (POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS))) is V17() V27() V28() Element of REAL
((y0 * K) + (POS * a)) + ((- 1) * ((y0 * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * y0)) + (POS * ((((K * y0) + (a * POS)) * (((y0 * y0) + (POS * POS)) ")) * POS)))) is V17() V27() V28() Element of REAL
(((y0 * y0) + (POS * POS)) ") * ((y0 * y0) + (POS * POS)) is V17() V27() V28() Element of REAL
((K * y0) + (a * POS)) * ((((y0 * y0) + (POS * POS)) ") * ((y0 * y0) + (POS * POS))) is V17() V27() V28() Element of REAL
(- 1) * (((K * y0) + (a * POS)) * ((((y0 * y0) + (POS * POS)) ") * ((y0 * y0) + (POS * POS)))) is V17() V27() V28() Element of REAL
((K * y0) + (a * POS)) * 1 is V17() V27() V28() Element of REAL
(- 1) * (((K * y0) + (a * POS)) * 1) is V17() V27() V28() Element of REAL
- ((y0 * K) + (POS * a)) is V17() V27() V28() Element of REAL
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
y0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,y0,(- w0)) is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
w0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,w0,(- V0)) is Element of the carrier of V0
POS is Element of the carrier of V0
y0 is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
a is Element of the carrier of V0
K is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (a - K) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
POS is Element of the carrier of V0
y0 is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
a is Element of the carrier of V0
K is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (a - K) is Element of the carrier of V0
K - a is Element of the carrier of V0
- a is Element of the carrier of V0
K176(V0,K,(- a)) is Element of the carrier of V0
- (K - a) is Element of the carrier of V0
q * (- (K - a)) is Element of the carrier of V0
- q is V17() V27() V28() Element of REAL
(- q) * (K - a) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (w0 - V0) is Element of the carrier of V0
- y0 is V17() V27() V28() Element of REAL
- POS is V17() V27() V28() Element of REAL
w0 - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,w0,(- y0)) is Element of the carrier of V0
(- y0) * (w0 - y0) is Element of the carrier of V0
- (w0 - y0) is Element of the carrier of V0
y0 * (- (w0 - y0)) is Element of the carrier of V0
V0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,V0,(- w0)) is Element of the carrier of V0
- (V0 - w0) is Element of the carrier of V0
POS * (- (V0 - w0)) is Element of the carrier of V0
(- POS) * (V0 - w0) is Element of the carrier of V0
y0 is Element of the carrier of V0
POS is Element of the carrier of V0
K is Element of the carrier of V0
a is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
1 * (POS - y0) is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
0 * (a - K) is Element of the carrier of V0
1 * (a - K) is Element of the carrier of V0
0 * (POS - y0) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
q is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q * (a - K) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * (POS - y0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (a - K) is Element of the carrier of V0
x is V17() V27() V28() Element of REAL
x * (POS - y0) is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * (a - K) is Element of the carrier of V0
c9 is V17() V27() V28() Element of REAL
c9 * (POS - y0) is Element of the carrier of V0
d9 is V17() V27() V28() Element of REAL
d9 * (a - K) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (V0 - w0) is Element of the carrier of V0
- POS is V17() V27() V28() Element of REAL
(- POS) * (w0 - V0) is Element of the carrier of V0
- (w0 - V0) is Element of the carrier of V0
POS * (- (w0 - V0)) is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (w0 - V0) is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * (y0 - w0) is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * (w0 - V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
[: the carrier of V0, the carrier of V0:] is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
[w0,y0] is Element of [: the carrier of V0, the carrier of V0:]
y0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,y0,(- w0)) is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
[V0,w0] is Element of [: the carrier of V0, the carrier of V0:]
[[w0,y0],[V0,w0]] is Element of [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,w0,(- V0)) is Element of the carrier of V0
[w0,V0] is Element of [: the carrier of V0, the carrier of V0:]
[[w0,y0],[w0,V0]] is Element of [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
y0 is V17() V27() V28() Element of REAL
y0 * (y0 - w0) is Element of the carrier of V0
POS is V17() V27() V28() Element of REAL
POS * (w0 - V0) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
y0 is set
POS is set
[y0,POS] is set
K is Element of the carrier of V0
a is Element of the carrier of V0
[K,a] is Element of [: the carrier of V0, the carrier of V0:]
p is Element of the carrier of V0
q is Element of the carrier of V0
[p,q] is Element of [: the carrier of V0, the carrier of V0:]
V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
y0 is set
POS is set
[y0,POS] is set
K is Element of the carrier of V0
a is Element of the carrier of V0
[K,a] is Element of [: the carrier of V0, the carrier of V0:]
p is Element of the carrier of V0
q is Element of the carrier of V0
[p,q] is Element of [: the carrier of V0, the carrier of V0:]
K is Element of the carrier of V0
a is Element of the carrier of V0
[K,a] is Element of [: the carrier of V0, the carrier of V0:]
p is Element of the carrier of V0
q is Element of the carrier of V0
[p,q] is Element of [: the carrier of V0, the carrier of V0:]
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
the carrier of (Lambda (OASpace V0)) is non empty set
the carrier of V0 is non empty set
the carrier of (OASpace V0) is non empty set
the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
[: the carrier of (OASpace V0), the carrier of (OASpace V0):] is non empty set
[:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
lambda the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
AffinStruct(# the carrier of (OASpace V0),(lambda the CONGR of (OASpace V0)) #) is strict AffinStruct
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
AffinStruct(# the carrier of V0,(DirPar V0) #) is strict AffinStruct
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
the CONGR of (Lambda (OASpace V0)) is V7() V10([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) V11([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) Element of bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:]
the carrier of (Lambda (OASpace V0)) is non empty set
[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):] is non empty set
[:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
the carrier of V0 is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
the carrier of (OASpace V0) is non empty set
the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
[: the carrier of (OASpace V0), the carrier of (OASpace V0):] is non empty set
[:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:] is non empty set
lambda the CONGR of (OASpace V0) is V7() V10([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) V11([: the carrier of (OASpace V0), the carrier of (OASpace V0):]) Element of bool [:[: the carrier of (OASpace V0), the carrier of (OASpace V0):],[: the carrier of (OASpace V0), the carrier of (OASpace V0):]:]
AffinStruct(# the carrier of (OASpace V0),(lambda the CONGR of (OASpace V0)) #) is strict AffinStruct
AffinStruct(# the carrier of V0,(DirPar V0) #) is strict AffinStruct
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
the carrier of (Lambda (OASpace V0)) is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
y0 - w0 is Element of the carrier of V0
- w0 is Element of the carrier of V0
K176(V0,y0,(- w0)) is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
w0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,w0,(- V0)) is Element of the carrier of V0
y0 is Element of the carrier of (Lambda (OASpace V0))
POS is Element of the carrier of (Lambda (OASpace V0))
K is Element of the carrier of (Lambda (OASpace V0))
a is Element of the carrier of (Lambda (OASpace V0))
[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):] is non empty set
[y0,POS] is Element of [: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]
[K,a] is Element of [: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]
[[y0,POS],[K,a]] is Element of [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:]
[:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
the CONGR of (Lambda (OASpace V0)) is V7() V10([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) V11([: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]) Element of bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:]
bool [:[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):],[: the carrier of (Lambda (OASpace V0)), the carrier of (Lambda (OASpace V0)):]:] is non empty set
[: the carrier of V0, the carrier of V0:] is non empty set
[w0,y0] is Element of [: the carrier of V0, the carrier of V0:]
[V0,w0] is Element of [: the carrier of V0, the carrier of V0:]
[[w0,y0],[V0,w0]] is Element of [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
p is V17() V27() V28() Element of REAL
p * (y0 - w0) is Element of the carrier of V0
q is V17() V27() V28() Element of REAL
q * (w0 - V0) is Element of the carrier of V0
the non empty set is non empty set
[: the non empty set , the non empty set :] is non empty set
[:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:] is non empty set
bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:] is non empty set
the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:] is V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:]
( the non empty set , the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:], the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:]) is () ()
the carrier of ( the non empty set , the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:], the V7() V10([: the non empty set , the non empty set :]) V11([: the non empty set , the non empty set :]) Element of bool [:[: the non empty set , the non empty set :],[: the non empty set , the non empty set :]:]) is set
V0 is non empty ()
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
POS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of POS is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the CONGR of (V0,w0,y0) is V7() V10([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) V11([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) Element of bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
the carrier of (V0,w0,y0) is non empty set
[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):] is non empty set
[:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
(POS,K,a) is non empty () ()
DirPar POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
lambda (DirPar POS) is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
(POS,K,a) is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
( the carrier of POS,(lambda (DirPar POS)),(POS,K,a)) is () ()
the of (POS,K,a) is V7() V10([: the carrier of (POS,K,a), the carrier of (POS,K,a):]) V11([: the carrier of (POS,K,a), the carrier of (POS,K,a):]) Element of bool [:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:]
the carrier of (POS,K,a) is non empty set
[: the carrier of (POS,K,a), the carrier of (POS,K,a):] is non empty set
[:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:] is non empty set
bool [:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:] is non empty set
V0 is non empty ()
the carrier of V0 is non empty set
the CONGR of V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
AffinStruct(# the carrier of V0, the CONGR of V0 #) is strict AffinStruct
V0 is non empty ()
(V0) is strict AffinStruct
the carrier of V0 is non empty set
the CONGR of V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
AffinStruct(# the carrier of V0, the CONGR of V0 #) is strict AffinStruct
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
((V0,w0,y0)) is non empty strict AffinStruct
the carrier of (V0,w0,y0) is non empty set
the CONGR of (V0,w0,y0) is V7() V10([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) V11([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) Element of bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):] is non empty set
[:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
AffinStruct(# the carrier of (V0,w0,y0), the CONGR of (V0,w0,y0) #) is strict AffinStruct
the carrier of (Lambda (OASpace V0)) is non empty set
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
POS is Element of the carrier of V0
(V0,y0,POS) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,y0,POS) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,y0,POS)) is () ()
the carrier of (V0,y0,POS) is non empty set
K is Element of the carrier of (V0,y0,POS)
a is Element of the carrier of (V0,y0,POS)
p is Element of the carrier of (V0,y0,POS)
q is Element of the carrier of (V0,y0,POS)
[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):] is non empty set
[K,p] is Element of [: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]
[a,q] is Element of [: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]
[[K,p],[a,q]] is Element of [:[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):],[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]:]
[:[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):],[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]:] is non empty set
the of (V0,y0,POS) is V7() V10([: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]) V11([: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]) Element of bool [:[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):],[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]:]
bool [:[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):],[: the carrier of (V0,y0,POS), the carrier of (V0,y0,POS):]:] is non empty set
[w0,V0] is Element of [: the carrier of V0, the carrier of V0:]
[y0,w0] is Element of [: the carrier of V0, the carrier of V0:]
x is Element of the carrier of V0
c₁₃ is Element of the carrier of V0
[x,c₁₃] is Element of [: the carrier of V0, the carrier of V0:]
c9 is Element of the carrier of V0
d9 is Element of the carrier of V0
[c9,d9] is Element of [: the carrier of V0, the carrier of V0:]
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of V0
w0 is Element of the carrier of V0
w0 - V0 is Element of the carrier of V0
- V0 is Element of the carrier of V0
K176(V0,w0,(- V0)) is Element of the carrier of V0
y0 is Element of the carrier of V0
POS is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
K is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
q is Element of the carrier of (V0,w0,y0)
[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):] is non empty set
[K,a] is Element of [: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]
[p,q] is Element of [: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]
[[K,a],[p,q]] is Element of [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
[:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
the CONGR of (V0,w0,y0) is V7() V10([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) V11([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) Element of bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
x is V17() V27() V28() Element of REAL
x * (w0 - V0) is Element of the carrier of V0
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * (POS - y0) is Element of the carrier of V0
[V0,w0] is Element of [: the carrier of V0, the carrier of V0:]
[y0,POS] is Element of [: the carrier of V0, the carrier of V0:]
[[V0,w0],[y0,POS]] is Element of [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
POS is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of V0
a is Element of the carrier of V0
p is Element of the carrier of V0
q is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
q - p is Element of the carrier of V0
- p is Element of the carrier of V0
K176(V0,q,(- p)) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
POS is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of V0
a is Element of the carrier of V0
p is Element of the carrier of V0
q is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
q - p is Element of the carrier of V0
- p is Element of the carrier of V0
K176(V0,q,(- p)) is Element of the carrier of V0
(- 1) * (q - p) is Element of the carrier of V0
- (q - p) is Element of the carrier of V0
p - q is Element of the carrier of V0
- q is Element of the carrier of V0
K176(V0,p,(- q)) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of V0
a - a is Element of the carrier of V0
- a is Element of the carrier of V0
K176(V0,a,(- a)) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
K is Element of the carrier of V0
POS is Element of the carrier of V0
K - POS is Element of the carrier of V0
- POS is Element of the carrier of V0
K176(V0,K,(- POS)) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
POS is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of (V0,w0,y0)
q is Element of the carrier of V0
p is Element of the carrier of V0
q - p is Element of the carrier of V0
- p is Element of the carrier of V0
K176(V0,q,(- p)) is Element of the carrier of V0
d9 is Element of the carrier of V0
c9 is Element of the carrier of V0
d9 - c9 is Element of the carrier of V0
- c9 is Element of the carrier of V0
K176(V0,d9,(- c9)) is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * (q - p) is Element of the carrier of V0
N is V17() V27() V28() Element of REAL
N * (d9 - c9) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
N " is V17() V27() V28() Element of REAL
(N ") * (M * (q - p)) is Element of the carrier of V0
(N ") * M is V17() V27() V28() Element of REAL
((N ") * M) * (q - p) is Element of the carrier of V0
x is Element of the carrier of V0
c₁₃ is Element of the carrier of V0
c₁₃ - x is Element of the carrier of V0
- x is Element of the carrier of V0
K176(V0,c₁₃,(- x)) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of V0
POS is Element of the carrier of V0
K - POS is Element of the carrier of V0
- POS is Element of the carrier of V0
K176(V0,K,(- POS)) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
p is Element of the carrier of V0
a is Element of the carrier of V0
a + p is Element of the carrier of V0
(a + p) - a is Element of the carrier of V0
- a is Element of the carrier of V0
K176(V0,(a + p),(- a)) is Element of the carrier of V0
a - a is Element of the carrier of V0
K176(V0,a,(- a)) is Element of the carrier of V0
p + (a - a) is Element of the carrier of V0
p + (0. V0) is Element of the carrier of V0
x is Element of the carrier of (V0,w0,y0)
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
POS is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of V0
q is Element of the carrier of V0
c9 is Element of the carrier of V0
d9 is Element of the carrier of V0
q - p is Element of the carrier of V0
- p is Element of the carrier of V0
K176(V0,q,(- p)) is Element of the carrier of V0
d9 - c9 is Element of the carrier of V0
- c9 is Element of the carrier of V0
K176(V0,d9,(- c9)) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
x is Element of the carrier of V0
c₁₃ is Element of the carrier of V0
c₁₃ - x is Element of the carrier of V0
- x is Element of the carrier of V0
K176(V0,c₁₃,(- x)) is Element of the carrier of V0
M is V17() V27() V28() Element of REAL
M * (c₁₃ - x) is Element of the carrier of V0
N is V17() V27() V28() Element of REAL
N * (d9 - c9) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
POS is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of V0
p is Element of the carrier of V0
q is Element of the carrier of V0
c₁₃ is Element of the carrier of V0
p - a is Element of the carrier of V0
- a is Element of the carrier of V0
K176(V0,p,(- a)) is Element of the carrier of V0
c₁₃ - q is Element of the carrier of V0
- q is Element of the carrier of V0
K176(V0,c₁₃,(- q)) is Element of the carrier of V0
x is Element of the carrier of V0
x - q is Element of the carrier of V0
K176(V0,x,(- q)) is Element of the carrier of V0
(c₁₃ - q) - (x - q) is Element of the carrier of V0
- (x - q) is Element of the carrier of V0
K176(V0,(c₁₃ - q),(- (x - q))) is Element of the carrier of V0
(x - q) + q is Element of the carrier of V0
c₁₃ - ((x - q) + q) is Element of the carrier of V0
- ((x - q) + q) is Element of the carrier of V0
K176(V0,c₁₃,(- ((x - q) + q))) is Element of the carrier of V0
q - q is Element of the carrier of V0
K176(V0,q,(- q)) is Element of the carrier of V0
x - (q - q) is Element of the carrier of V0
- (q - q) is Element of the carrier of V0
K176(V0,x,(- (q - q))) is Element of the carrier of V0
c₁₃ - (x - (q - q)) is Element of the carrier of V0
- (x - (q - q)) is Element of the carrier of V0
K176(V0,c₁₃,(- (x - (q - q)))) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
x - (0. V0) is Element of the carrier of V0
- (0. V0) is Element of the carrier of V0
K176(V0,x,(- (0. V0))) is Element of the carrier of V0
c₁₃ - (x - (0. V0)) is Element of the carrier of V0
- (x - (0. V0)) is Element of the carrier of V0
K176(V0,c₁₃,(- (x - (0. V0)))) is Element of the carrier of V0
c₁₃ - x is Element of the carrier of V0
- x is Element of the carrier of V0
K176(V0,c₁₃,(- x)) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of V0
POS is Element of the carrier of V0
POS - y0 is Element of the carrier of V0
- y0 is Element of the carrier of V0
K176(V0,POS,(- y0)) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
POS is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of V0
a is Element of the carrier of V0
p is Element of the carrier of V0
q is Element of the carrier of V0
a - K is Element of the carrier of V0
- K is Element of the carrier of V0
K176(V0,a,(- K)) is Element of the carrier of V0
q - p is Element of the carrier of V0
- p is Element of the carrier of V0
K176(V0,q,(- p)) is Element of the carrier of V0
a - p is Element of the carrier of V0
K176(V0,a,(- p)) is Element of the carrier of V0
K - q is Element of the carrier of V0
- q is Element of the carrier of V0
K176(V0,K,(- q)) is Element of the carrier of V0
x is Element of the carrier of V0
c₁₃ is Element of the carrier of V0
x - c₁₃ is Element of the carrier of V0
- c₁₃ is Element of the carrier of V0
K176(V0,x,(- c₁₃)) is Element of the carrier of V0
c9 is Element of the carrier of V0
x - c9 is Element of the carrier of V0
- c9 is Element of the carrier of V0
K176(V0,x,(- c9)) is Element of the carrier of V0
(x - c₁₃) - (x - c9) is Element of the carrier of V0
- (x - c9) is Element of the carrier of V0
K176(V0,(x - c₁₃),(- (x - c9))) is Element of the carrier of V0
c9 - x is Element of the carrier of V0
- x is Element of the carrier of V0
K176(V0,c9,(- x)) is Element of the carrier of V0
(c9 - x) + (x - c₁₃) is Element of the carrier of V0
c9 - c₁₃ is Element of the carrier of V0
K176(V0,c9,(- c₁₃)) is Element of the carrier of V0
(a - K) - (a - p) is Element of the carrier of V0
- (a - p) is Element of the carrier of V0
K176(V0,(a - K),(- (a - p))) is Element of the carrier of V0
p - K is Element of the carrier of V0
K176(V0,p,(- K)) is Element of the carrier of V0
a - q is Element of the carrier of V0
K176(V0,a,(- q)) is Element of the carrier of V0
(a - p) - (a - q) is Element of the carrier of V0
- (a - q) is Element of the carrier of V0
K176(V0,(a - p),(- (a - q))) is Element of the carrier of V0
(a - q) - (a - K) is Element of the carrier of V0
- (a - K) is Element of the carrier of V0
K176(V0,(a - q),(- (a - K))) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
V0 is Element of the carrier of (V0,w0,y0)
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of V0
POS is Element of the carrier of V0
a - POS is Element of the carrier of V0
- POS is Element of the carrier of V0
K176(V0,a,(- POS)) is Element of the carrier of V0
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
K is Element of the carrier of V0
K - POS is Element of the carrier of V0
K176(V0,K,(- POS)) is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * (a - POS) is Element of the carrier of V0
(K - POS) - (p * (a - POS)) is Element of the carrier of V0
- (p * (a - POS)) is Element of the carrier of V0
K176(V0,(K - POS),(- (p * (a - POS)))) is Element of the carrier of V0
POS + (p * (a - POS)) is Element of the carrier of V0
K - (POS + (p * (a - POS))) is Element of the carrier of V0
- (POS + (p * (a - POS))) is Element of the carrier of V0
K176(V0,K,(- (POS + (p * (a - POS))))) is Element of the carrier of V0
x is Element of the carrier of (V0,w0,y0)
(p * (a - POS)) + (0. V0) is Element of the carrier of V0
POS - POS is Element of the carrier of V0
K176(V0,POS,(- POS)) is Element of the carrier of V0
(p * (a - POS)) + (POS - POS) is Element of the carrier of V0
(POS + (p * (a - POS))) - POS is Element of the carrier of V0
K176(V0,(POS + (p * (a - POS))),(- POS)) is Element of the carrier of V0
1 * ((POS + (p * (a - POS))) - POS) is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
the CONGR of (V0,w0,y0) is V7() V10([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) V11([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) Element of bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):] is non empty set
[:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
AffinStruct(# the carrier of (V0,w0,y0), the CONGR of (V0,w0,y0) #) is strict AffinStruct
((V0,w0,y0)) is non empty strict AffinStruct
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
w0 is V17() V27() V28() Element of REAL
w0 * w0 is Element of the carrier of V0
y0 is V17() V27() V28() Element of REAL
y0 * y0 is Element of the carrier of V0
(w0 * w0) + (y0 * y0) is Element of the carrier of V0
w0 is Element of the carrier of (V0,w0,y0)
y0 is Element of the carrier of (V0,w0,y0)
POS is Element of the carrier of (V0,w0,y0)
K is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
q is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
c₁₃ is Element of the carrier of (V0,w0,y0)
c9 is Element of the carrier of (V0,w0,y0)
d9 is Element of the carrier of (V0,w0,y0)
M is Element of the carrier of (V0,w0,y0)
N is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
p19 is Element of the carrier of (V0,w0,y0)
p29 is Element of the carrier of (V0,w0,y0)
q19 is Element of the carrier of (V0,w0,y0)
q29 is Element of the carrier of (V0,w0,y0)
q19 is Element of the carrier of (V0,w0,y0)
p29 is Element of the carrier of (V0,w0,y0)
q29 is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
x9 is Element of the carrier of (V0,w0,y0)
y9 is Element of the carrier of (V0,w0,y0)
z9 is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
the CONGR of (V0,w0,y0) is V7() V10([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) V11([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) Element of bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):] is non empty set
[:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
AffinStruct(# the carrier of (V0,w0,y0), the CONGR of (V0,w0,y0) #) is strict AffinStruct
a is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
q is Element of the carrier of (V0,w0,y0)
((V0,w0,y0)) is non empty strict AffinStruct
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * w0 is Element of the carrier of V0
p is V17() V27() V28() Element of REAL
p * y0 is Element of the carrier of V0
(a * w0) + (p * y0) is Element of the carrier of V0
a is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
q is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
c₁₃ is Element of the carrier of (V0,w0,y0)
c9 is Element of the carrier of (V0,w0,y0)
d9 is Element of the carrier of (V0,w0,y0)
M is Element of the carrier of (V0,w0,y0)
N is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
p19 is Element of the carrier of (V0,w0,y0)
p29 is Element of the carrier of (V0,w0,y0)
q19 is Element of the carrier of (V0,w0,y0)
q29 is Element of the carrier of (V0,w0,y0)
q19 is Element of the carrier of (V0,w0,y0)
p29 is Element of the carrier of (V0,w0,y0)
q29 is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
x9 is Element of the carrier of (V0,w0,y0)
y9 is Element of the carrier of (V0,w0,y0)
z9 is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
y is Element of the carrier of (V0,w0,y0)
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
V0 is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V0 is non empty set
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
w0 is Element of the carrier of V0
y0 is Element of the carrier of V0
(V0,w0,y0) is non empty () ()
DirPar V0 is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
[: the carrier of V0, the carrier of V0:] is non empty set
[:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:] is non empty set
lambda (DirPar V0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
(V0,w0,y0) is V7() V10([: the carrier of V0, the carrier of V0:]) V11([: the carrier of V0, the carrier of V0:]) Element of bool [:[: the carrier of V0, the carrier of V0:],[: the carrier of V0, the carrier of V0:]:]
( the carrier of V0,(lambda (DirPar V0)),(V0,w0,y0)) is () ()
the carrier of (V0,w0,y0) is non empty set
the CONGR of (V0,w0,y0) is V7() V10([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) V11([: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]) Element of bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:]
[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):] is non empty set
[:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
bool [:[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):],[: the carrier of (V0,w0,y0), the carrier of (V0,w0,y0):]:] is non empty set
AffinStruct(# the carrier of (V0,w0,y0), the CONGR of (V0,w0,y0) #) is strict AffinStruct
((V0,w0,y0)) is non empty strict AffinStruct
OASpace V0 is non empty strict AffinStruct
Lambda (OASpace V0) is non empty strict AffinStruct
0. V0 is V59(V0) Element of the carrier of V0
the ZeroF of V0 is Element of the carrier of V0
K is V17() V27() V28() Element of REAL
K * w0 is Element of the carrier of V0
a is V17() V27() V28() Element of REAL
a * y0 is Element of the carrier of V0
(K * w0) + (a * y0) is Element of the carrier of V0
p is Element of the carrier of V0
K is Element of the carrier of (V0,w0,y0)
a is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
q is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
c₁₃ is Element of the carrier of (V0,w0,y0)
c9 is Element of the carrier of (V0,w0,y0)
d9 is Element of the carrier of (V0,w0,y0)
M is Element of the carrier of (V0,w0,y0)
N is Element of the carrier of (V0,w0,y0)
p is Element of the carrier of (V0,w0,y0)
p19 is Element of the carrier of (V0,w0,y0)
p29 is Element of the carrier of (V0,w0,y0)
q19 is Element of the carrier of (V0,w0,y0)
q29 is Element of the carrier of (V0,w0,y0)
q19 is Element of the carrier of (V0,w0,y0)
p29 is Element of the carrier of (V0,w0,y0)
q29 is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
x9 is Element of the carrier of (V0,w0,y0)
y9 is Element of the carrier of (V0,w0,y0)
z9 is Element of the carrier of (V0,w0,y0)
x is Element of the carrier of (V0,w0,y0)
y is Element of the carrier of (V0,w0,y0)
POS is non empty V78() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
(POS,K,a) is non empty () ()
DirPar POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
lambda (DirPar POS) is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
(POS,K,a) is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
( the carrier of POS,(lambda (DirPar POS)),(POS,K,a)) is () ()
the carrier of (POS,K,a) is non empty set
the CONGR of (POS,K,a) is V7() V10([: the carrier of (POS,K,a), the carrier of (POS,K,a):]) V11([: the carrier of (POS,K,a), the carrier of (POS,K,a):]) Element of bool [:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:]
[: the carrier of (POS,K,a), the carrier of (POS,K,a):] is non empty set
[:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:] is non empty set
bool [:[: the carrier of (POS,K,a), the carrier of (POS,K,a):],[: the carrier of (POS,K,a), the carrier of (POS,K,a):]:] is non empty set
AffinStruct(# the carrier of (POS,K,a), the CONGR of (POS,K,a) #) is strict AffinStruct
((POS,K,a)) is non empty strict AffinStruct
OASpace POS is non empty strict AffinStruct
Lambda (OASpace POS) is non empty strict AffinStruct
0. POS is V59(POS) Element of the carrier of POS
the ZeroF of POS is Element of the carrier of POS
x is V17() V27() V28() Element of REAL
x * K is Element of the carrier of POS
c₁₃ is V17() V27() V28() Element of REAL
c₁₃ * a is Element of the carrier of POS
(x * K) + (c₁₃ * a) is Element of the carrier of POS
c9 is Element of the carrier of POS
x is Element of the carrier of (POS,K,a)
c₁₃ is Element of the carrier of (POS,K,a)
c9 is Element of the carrier of (POS,K,a)
d9 is Element of the carrier of (POS,K,a)
M is Element of the carrier of (POS,K,a)
N is Element of the carrier of (POS,K,a)
p is Element of the carrier of (POS,K,a)
p19 is Element of the carrier of (POS,K,a)
p29 is Element of the carrier of (POS,K,a)
q19 is Element of the carrier of (POS,K,a)
q29 is Element of the carrier of (POS,K,a)
q19 is Element of the carrier of (POS,K,a)
p29 is Element of the carrier of (POS,K,a)
q29 is Element of the carrier of (POS,K,a)
x is Element of the carrier of (POS,K,a)
x9 is Element of the carrier of (POS,K,a)
y9 is Element of the carrier of (POS,K,a)
z9 is Element of the carrier of (POS,K,a)
x is Element of the carrier of (POS,K,a)
y is Element of the carrier of (POS,K,a)
z is Element of the carrier of (POS,K,a)
x9 is Element of the carrier of (POS,K,a)
x is Element of the carrier of (POS,K,a)
x9 is Element of the carrier of (POS,K,a)
K is set
POS is non empty ()
the carrier of POS is non empty set
(POS) is non empty strict AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty set
p is set
a is non empty ()
(a) is non empty strict AffinStruct
the carrier of a is non empty set
the CONGR of a is V7() V10([: the carrier of a, the carrier of a:]) V11([: the carrier of a, the carrier of a:]) Element of bool [:[: the carrier of a, the carrier of a:],[: the carrier of a, the carrier of a:]:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:],[: the carrier of a, the carrier of a:]:] is non empty set
bool [:[: the carrier of a, the carrier of a:],[: the carrier of a, the carrier of a:]:] is non empty set
AffinStruct(# the carrier of a, the CONGR of a #) is strict AffinStruct
the carrier of (a) is non empty set
POS is non empty ()
the carrier of POS is non empty set
(POS) is non empty strict AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty set
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
M is Element of the carrier of (POS)
[: the carrier of (POS), the carrier of (POS):] is non empty set
[c₁₃,c9] is Element of [: the carrier of (POS), the carrier of (POS):]
[d9,M] is Element of [: the carrier of (POS), the carrier of (POS):]
[[c₁₃,c9],[d9,M]] is Element of [:[: the carrier of (POS), the carrier of (POS):],[: the carrier of (POS), the carrier of (POS):]:]
[:[: the carrier of (POS), the carrier of (POS):],[: the carrier of (POS), the carrier of (POS):]:] is non empty set
the CONGR of (POS) is V7() V10([: the carrier of (POS), the carrier of (POS):]) V11([: the carrier of (POS), the carrier of (POS):]) Element of bool [:[: the carrier of (POS), the carrier of (POS):],[: the carrier of (POS), the carrier of (POS):]:]
bool [:[: the carrier of (POS), the carrier of (POS):],[: the carrier of (POS), the carrier of (POS):]:] is non empty set
[a,p] is Element of [: the carrier of POS, the carrier of POS:]
[q,x] is Element of [: the carrier of POS, the carrier of POS:]
[[a,p],[q,x]] is Element of [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
POS is non empty () ()
(POS) is non empty strict AffinStruct
the carrier of POS is non empty set
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
POS is non empty () ()
(POS) is non empty strict AffinStruct
the carrier of POS is non empty set
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
POS is non empty () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
d9 is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like 2-dimensional AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
M is Element of the carrier of (POS)
N is Element of the carrier of (POS)
p is Element of the carrier of (POS)
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
p19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q19 is Element of the carrier of POS
q29 is Element of the carrier of POS
q19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q29 is Element of the carrier of POS
x is Element of the carrier of POS
x9 is Element of the carrier of POS
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like 2-dimensional AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
M is Element of the carrier of (POS)
N is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like 2-dimensional AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
POS is non empty ()
POS is non empty () ()
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the carrier of POS is non empty set
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
the carrier of (POS) is non empty non trivial set
p is Element of the carrier of (POS)
p19 is Element of the carrier of (POS)
p29 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
q19 is Element of the carrier of POS
M is Element of the carrier of (POS)
N is Element of the carrier of (POS)
p29 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
x is Element of the carrier of POS
p29 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
x is Element of the carrier of POS
p29 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
x is Element of the carrier of POS
p29 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
x is Element of the carrier of POS
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
POS is non empty ()
the carrier of POS is non empty set
(POS) is non empty strict AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty set
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of (POS)
p is Element of the carrier of (POS)
p19 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
p29 is Element of the carrier of (POS)
x9 is Element of the carrier of (POS)
y9 is Element of the carrier of (POS)
z9 is Element of the carrier of (POS)
x is Element of the carrier of POS
x9 is Element of the carrier of (POS)
x is Element of the carrier of POS
y is Element of the carrier of POS
z is Element of the carrier of POS
x is Element of the carrier of POS
p29 is Element of the carrier of (POS)
x9 is Element of the carrier of (POS)
x is Element of the carrier of POS
x9 is Element of the carrier of (POS)
x is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of (POS)
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of POS
M is Element of the carrier of POS
d9 is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
p19 is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of (POS)
q is Element of the carrier of (POS)
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
M is Element of the carrier of (POS)
N is Element of the carrier of POS
p is Element of the carrier of POS
p19 is Element of the carrier of POS
q19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q29 is Element of the carrier of POS
p29 is Element of the carrier of POS
q19 is Element of the carrier of POS
q29 is Element of the carrier of POS
q19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q29 is Element of the carrier of POS
q19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q29 is Element of the carrier of POS
q is Element of the carrier of (POS)
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
p19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q19 is Element of the carrier of POS
p19 is Element of the carrier of POS
p29 is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
q is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
x is Element of the carrier of (POS)
N is Element of the carrier of POS
d9 is Element of the carrier of POS
p is Element of the carrier of POS
M is Element of the carrier of POS
p19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q19 is Element of the carrier of POS
p19 is Element of the carrier of POS
p29 is Element of the carrier of (POS)
q is Element of the carrier of (POS)
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
p19 is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of (POS)
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
M is Element of the carrier of (POS)
q is Element of the carrier of (POS)
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
p19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q19 is Element of the carrier of POS
q29 is Element of the carrier of POS
q19 is Element of the carrier of POS
p29 is Element of the carrier of POS
q29 is Element of the carrier of POS
x is Element of the carrier of POS
x9 is Element of the carrier of POS
y9 is Element of the carrier of POS
z9 is Element of the carrier of POS
x is Element of the carrier of POS
y is Element of the carrier of POS
z is Element of the carrier of POS
x9 is Element of the carrier of POS
x is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
POS is non empty ()
the carrier of POS is non empty set
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of bool the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
p is Element of bool the carrier of POS
q is Element of bool the carrier of POS
x is set
c₁₃ is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
POS is non empty () ()
the carrier of POS is non empty set
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of (POS)
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
K is Element of the carrier of POS
a is Element of the carrier of POS
(POS,K,a) is Element of bool the carrier of POS
bool the carrier of POS is non empty set
p is Element of the carrier of (POS)
q is Element of the carrier of (POS)
Line (p,q) is Element of bool the carrier of (POS)
bool the carrier of (POS) is non empty set
c9 is set
d9 is Element of the carrier of (POS)
M is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of (POS)
K is set
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
(POS) is non empty strict AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty set
bool the carrier of (POS) is non empty set
p is set
a is non empty ()
(a) is non empty strict AffinStruct
the carrier of a is non empty set
the CONGR of a is V7() V10([: the carrier of a, the carrier of a:]) V11([: the carrier of a, the carrier of a:]) Element of bool [:[: the carrier of a, the carrier of a:],[: the carrier of a, the carrier of a:]:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:],[: the carrier of a, the carrier of a:]:] is non empty set
bool [:[: the carrier of a, the carrier of a:],[: the carrier of a, the carrier of a:]:] is non empty set
AffinStruct(# the carrier of a, the CONGR of a #) is strict AffinStruct
the carrier of (a) is non empty set
bool the carrier of (a) is non empty set
bool the carrier of a is non empty set
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
bool the carrier of (POS) is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of (POS)
p is Element of the carrier of POS
q is Element of the carrier of POS
(POS,p,q) is Element of bool the carrier of POS
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
Line (x,c₁₃) is Element of bool the carrier of (POS)
p is Element of the carrier of (POS)
q is Element of the carrier of (POS)
Line (p,q) is Element of bool the carrier of (POS)
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of bool the carrier of POS
q is Element of bool the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of bool the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
(POS,d9,M) is Element of bool the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
POS is non empty ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
(POS,p,q) is Element of bool the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS,p,q) is Element of bool the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
bool the carrier of (POS) is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of bool the carrier of (POS)
q is Element of bool the carrier of (POS)
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
(POS,c9,d9) is Element of bool the carrier of POS
M is Element of the carrier of (POS)
N is Element of the carrier of (POS)
p is Element of the carrier of (POS)
p19 is Element of the carrier of (POS)
Line (M,N) is Element of bool the carrier of (POS)
Line (p,p19) is Element of bool the carrier of (POS)
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
Line (x,c₁₃) is Element of bool the carrier of (POS)
Line (c9,d9) is Element of bool the carrier of (POS)
M is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
p19 is Element of the carrier of POS
(POS,M,N) is Element of bool the carrier of POS
(POS,p,p19) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
(POS,p,q) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
N is Element of the carrier of POS
p is Element of the carrier of POS
(POS,N,p) is Element of bool the carrier of POS
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
M is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
(POS,q,x) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
p is Element of bool the carrier of POS
q is Element of bool the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
(POS,c9,d9) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
M is Element of the carrier of (POS)
N is Element of the carrier of (POS)
p is Element of the carrier of (POS)
p19 is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of POS
(POS,c9,d9) is Element of bool the carrier of POS
(POS,M,N) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
p29 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
Line (p29,q19) is Element of bool the carrier of (POS)
bool the carrier of (POS) is non empty set
p is Element of the carrier of (POS)
p19 is Element of the carrier of (POS)
Line (p,p19) is Element of bool the carrier of (POS)
q29 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
(POS,q,x) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
d9 is Element of the carrier of (POS)
M is Element of the carrier of (POS)
Line (d9,M) is Element of bool the carrier of (POS)
bool the carrier of (POS) is non empty set
c9 is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
p is Element of bool the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
(POS,q,x) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
Line (c₁₃,c9) is Element of bool the carrier of (POS)
bool the carrier of (POS) is non empty set
p is Element of bool the carrier of POS
q is Element of bool the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
(POS,c9,d9) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of bool the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
(POS,q,x) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
(POS,c₁₃,c9) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
N is Element of the carrier of (POS)
p is Element of the carrier of (POS)
M is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
(POS,a,p) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
bool the carrier of (POS) is non empty set
c₁₃ is Element of bool the carrier of (POS)
q is Element of the carrier of (POS)
x is Element of the carrier of (POS)
Line (q,x) is Element of bool the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
(POS,a,p) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of POS
(POS,c9,d9) is Element of bool the carrier of POS
(POS,M,N) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
q29 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
p19 is Element of the carrier of (POS)
p is Element of the carrier of (POS)
p29 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
p29 is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of bool the carrier of POS
q is Element of bool the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
(POS,d9,M) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
N is Element of the carrier of (POS)
p is Element of the carrier of (POS)
Line (N,p) is Element of bool the carrier of (POS)
bool the carrier of (POS) is non empty set
(POS,c₁₃,c9) is Element of bool the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
q is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
M is Element of the carrier of (POS)
N is Element of the carrier of (POS)
p is Element of the carrier of (POS)
p19 is Element of the carrier of (POS)
POS is non empty () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
POS is non empty () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
POS is non empty () () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
POS is non empty () () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
(POS,p,q) is Element of bool the carrier of POS
(POS,x,c₁₃) is Element of bool the carrier of POS
POS is non empty () () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
p is Element of bool the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
c₁₃ is Element of the carrier of POS
c9 is Element of the carrier of POS
(POS,q,x) is Element of bool the carrier of POS
(POS,c₁₃,c9) is Element of bool the carrier of POS
d9 is Element of the carrier of POS
M is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
(POS,d9,M) is Element of bool the carrier of POS
(POS,N,p) is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like 2-dimensional AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
p19 is Element of the carrier of (POS)
q19 is Element of the carrier of (POS)
Line (p19,q19) is Element of bool the carrier of (POS)
bool the carrier of (POS) is non empty set
p29 is Element of the carrier of (POS)
q29 is Element of the carrier of (POS)
Line (p29,q29) is Element of bool the carrier of (POS)
POS is non empty () () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of bool the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like 2-dimensional AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
bool the carrier of (POS) is non empty set
p is Element of bool the carrier of (POS)
q is Element of bool the carrier of (POS)
POS is non empty () () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
(POS) is non empty non trivial strict AffinSpace-like 2-dimensional AffinStruct
the CONGR of POS is V7() V10([: the carrier of POS, the carrier of POS:]) V11([: the carrier of POS, the carrier of POS:]) Element of bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:]
[: the carrier of POS, the carrier of POS:] is non empty set
[:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
bool [:[: the carrier of POS, the carrier of POS:],[: the carrier of POS, the carrier of POS:]:] is non empty set
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct
the carrier of (POS) is non empty non trivial set
(POS,K,a) is Element of bool the carrier of POS
bool the carrier of POS is non empty set
(POS,p,q) is Element of bool the carrier of POS
p is Element of the carrier of POS
x is Element of the carrier of (POS)
c₁₃ is Element of the carrier of (POS)
c9 is Element of the carrier of (POS)
d9 is Element of the carrier of (POS)
M is Element of the carrier of POS
N is Element of the carrier of POS
p is Element of the carrier of POS
POS is non empty () () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
(POS,q,x) is Element of bool the carrier of POS
c₁₃ is Element of the carrier of POS
POS is non empty () () ()
the carrier of POS is non empty set
K is Element of the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
q is Element of the carrier of POS
q is Element of the carrier of POS
x is Element of the carrier of POS
POS is non empty () () ()
the carrier of POS is non empty set
bool the carrier of POS is non empty set
K is Element of bool the carrier of POS
a is Element of the carrier of POS
p is Element of the carrier of POS
q is Element of the carrier of POS
(POS,p,q) is Element of bool the carrier of POS
x is Element of the carrier of POS