:: PARSP_1 semantic presentation

K122() is Element of bool K118()
K118() is set
bool K118() is non empty set
K117() is set
bool K117() is non empty set
bool K122() is non empty set

1 is non empty set

the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
- (a - b) is Element of the carrier of PS
b - a is Element of the carrier of PS
- a is Element of the carrier of PS
b + (- a) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
b - a is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c - p is Element of the carrier of PS
(a - b) * (c - p) is Element of the carrier of PS
p - c is Element of the carrier of PS
(b - a) * (p - c) is Element of the carrier of PS
((a - b) * (c - p)) - ((b - a) * (p - c)) is Element of the carrier of PS
- (a - b) is Element of the carrier of PS
- (c - p) is Element of the carrier of PS
((a - b) * (c - p)) - ((a - b) * (c - p)) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
b - b is Element of the carrier of PS
a * (b - b) is Element of the carrier of PS
c is Element of the carrier of PS
c - c is Element of the carrier of PS
p is Element of the carrier of PS
(c - c) * p is Element of the carrier of PS
(a * (b - b)) - ((c - c) * p) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) - (c * p) is Element of the carrier of PS
q is Element of the carrier of PS
a * q is Element of the carrier of PS
c * q is Element of the carrier of PS
s is Element of the carrier of PS
s * p is Element of the carrier of PS
(a * q) - (s * p) is Element of the carrier of PS
s * b is Element of the carrier of PS
(c * q) - (s * b) is Element of the carrier of PS
a " is Element of the carrier of PS
(s * p) * (a ") is Element of the carrier of PS
p * (a ") is Element of the carrier of PS
s * (p * (a ")) is Element of the carrier of PS
c * s is Element of the carrier of PS
(c * s) * (p * (a ")) is Element of the carrier of PS
(c * p) * (a ") is Element of the carrier of PS
c * (p * (a ")) is Element of the carrier of PS
s * c is Element of the carrier of PS
(s * c) * (p * (a ")) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
b * a is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) - (c * p) is Element of the carrier of PS
p * c is Element of the carrier of PS
(p * c) - (b * a) is Element of the carrier of PS
- ((a * b) - (c * p)) is Element of the carrier of PS
- (b * a) is Element of the carrier of PS
(p * c) + (- (b * a)) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
b * c is Element of the carrier of PS
p is Element of the carrier of PS
p * a is Element of the carrier of PS
(b * c) - (p * a) is Element of the carrier of PS
q is Element of the carrier of PS
b * q is Element of the carrier of PS
p * q is Element of the carrier of PS
s is Element of the carrier of PS
s * a is Element of the carrier of PS
(b * q) - (s * a) is Element of the carrier of PS
s * c is Element of the carrier of PS
(p * q) - (s * c) is Element of the carrier of PS
a * p is Element of the carrier of PS
c * b is Element of the carrier of PS
(a * p) - (c * b) is Element of the carrier of PS
a * s is Element of the carrier of PS
q * b is Element of the carrier of PS
(a * s) - (q * b) is Element of the carrier of PS
c * s is Element of the carrier of PS
q * p is Element of the carrier of PS
(c * s) - (q * p) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
c is Element of the carrier of PS
c * a is Element of the carrier of PS
(c * a) * b is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) * (c * p) is Element of the carrier of PS
((c * a) * b) * p is Element of the carrier of PS
c * (a * b) is Element of the carrier of PS
(c * (a * b)) * p is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) - (c * p) is Element of the carrier of PS
q is Element of the carrier of PS
a * q is Element of the carrier of PS
c * q is Element of the carrier of PS
s is Element of the carrier of PS
(a * q) * s is Element of the carrier of PS
((a * q) * s) * b is Element of the carrier of PS
(c * q) * s is Element of the carrier of PS
((c * q) * s) * p is Element of the carrier of PS
(((a * q) * s) * b) - (((c * q) * s) * p) is Element of the carrier of PS
q * s is Element of the carrier of PS
(q * s) * (a * b) is Element of the carrier of PS
(q * s) * (c * p) is Element of the carrier of PS
(q * s) * ((a * b) - (c * p)) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
c is Element of the carrier of PS
a * c is Element of the carrier of PS
p is Element of the carrier of PS
c - p is Element of the carrier of PS
(a - b) * (c - p) is Element of the carrier of PS
a * p is Element of the carrier of PS
- (a * p) is Element of the carrier of PS
b * (c - p) is Element of the carrier of PS
- (b * (c - p)) is Element of the carrier of PS
(- (a * p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) + ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS
- b is Element of the carrier of PS
a + (- b) is Element of the carrier of PS
(a + (- b)) * (c - p) is Element of the carrier of PS
a * (c - p) is Element of the carrier of PS
(- b) * (c - p) is Element of the carrier of PS
(a * (c - p)) + ((- b) * (c - p)) is Element of the carrier of PS
(a * (c - p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) - (a * p) is Element of the carrier of PS
((a * c) - (a * p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) + (- (a * p)) is Element of the carrier of PS
((a * c) + (- (a * p))) + (- (b * (c - p))) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a + b is Element of the carrier of PS
c is Element of the carrier of PS
b + c is Element of the carrier of PS
a + (b + c) is Element of the carrier of PS
p is Element of the carrier of PS
c + p is Element of the carrier of PS
(a + b) + (c + p) is Element of the carrier of PS
(a + (b + c)) + p is Element of the carrier of PS
(a + b) + c is Element of the carrier of PS
((a + b) + c) + p is Element of the carrier of PS

the carrier of PS is non empty set
b is Element of the carrier of PS
a is Element of the carrier of PS
b + a is Element of the carrier of PS
c is Element of the carrier of PS
c + a is Element of the carrier of PS
(b + a) - (c + a) is Element of the carrier of PS
b - c is Element of the carrier of PS
- (c + a) is Element of the carrier of PS
(b + a) + (- (c + a)) is Element of the carrier of PS
- a is Element of the carrier of PS
- c is Element of the carrier of PS
(- a) + (- c) is Element of the carrier of PS
(b + a) + ((- a) + (- c)) is Element of the carrier of PS
(b + a) + (- a) is Element of the carrier of PS
((b + a) + (- a)) + (- c) is Element of the carrier of PS
a + (- a) is Element of the carrier of PS
b + (a + (- a)) is Element of the carrier of PS
(b + (a + (- a))) + (- c) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
b + (0. PS) is Element of the carrier of PS
(b + (0. PS)) + (- c) is Element of the carrier of PS
b + (- c) is Element of the carrier of PS

the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
a + b is Element of the carrier of PS
- b is Element of the carrier of PS
- a is Element of the carrier of PS
(- b) + (- a) is Element of the carrier of PS
- ((- b) + (- a)) is Element of the carrier of PS
- (a + b) is Element of the carrier of PS
- (- (a + b)) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
b - a is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c - p is Element of the carrier of PS
(a - b) * (c - p) is Element of the carrier of PS
q is Element of the carrier of PS
a - q is Element of the carrier of PS
b - q is Element of the carrier of PS
s is Element of the carrier of PS
c - s is Element of the carrier of PS
(a - q) * (c - s) is Element of the carrier of PS
((a - b) * (c - p)) - ((a - q) * (c - s)) is Element of the carrier of PS
s - p is Element of the carrier of PS
(b - a) * (s - p) is Element of the carrier of PS
s - c is Element of the carrier of PS
(b - q) * (s - c) is Element of the carrier of PS
((b - a) * (s - p)) - ((b - q) * (s - c)) is Element of the carrier of PS
a * c is Element of the carrier of PS
a * p is Element of the carrier of PS
- (a * p) is Element of the carrier of PS
b * (c - p) is Element of the carrier of PS
- (b * (c - p)) is Element of the carrier of PS
(- (a * p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) + ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS
a * s is Element of the carrier of PS
- (a * s) is Element of the carrier of PS
q * (c - s) is Element of the carrier of PS
- (q * (c - s)) is Element of the carrier of PS
(- (a * s)) + (- (q * (c - s))) is Element of the carrier of PS
(a * c) + ((- (a * s)) + (- (q * (c - s)))) is Element of the carrier of PS
b * s is Element of the carrier of PS
b * p is Element of the carrier of PS
- (b * p) is Element of the carrier of PS
a * (s - p) is Element of the carrier of PS
- (a * (s - p)) is Element of the carrier of PS
(- (b * p)) + (- (a * (s - p))) is Element of the carrier of PS
(b * s) + ((- (b * p)) + (- (a * (s - p)))) is Element of the carrier of PS
b * c is Element of the carrier of PS
- (b * c) is Element of the carrier of PS
q * (s - c) is Element of the carrier of PS
- (q * (s - c)) is Element of the carrier of PS
(- (b * c)) + (- (q * (s - c))) is Element of the carrier of PS
(b * s) + ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
((- (b * p)) + (- (a * (s - p)))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(a * s) - (a * p) is Element of the carrier of PS
- ((a * s) - (a * p)) is Element of the carrier of PS
(- (b * p)) + (- ((a * s) - (a * p))) is Element of the carrier of PS
((- (b * p)) + (- ((a * s) - (a * p)))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(- (a * s)) + (a * p) is Element of the carrier of PS
(- (b * p)) + ((- (a * s)) + (a * p)) is Element of the carrier of PS
((- (b * p)) + ((- (a * s)) + (a * p))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(- (b * p)) + (a * p) is Element of the carrier of PS
((- (b * p)) + (a * p)) + (- (a * s)) is Element of the carrier of PS
(((- (b * p)) + (a * p)) + (- (a * s))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(a * p) + (- (b * p)) is Element of the carrier of PS
((a * p) + (- (b * p))) + (- (a * s)) is Element of the carrier of PS
- ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + (- ((- (b * c)) + (- (q * (s - c))))) is Element of the carrier of PS
- (- (b * c)) is Element of the carrier of PS
- (- (q * (s - c))) is Element of the carrier of PS
(- (- (b * c))) + (- (- (q * (s - c)))) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + ((- (- (b * c))) + (- (- (q * (s - c))))) is Element of the carrier of PS
(b * c) + (- (- (q * (s - c)))) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + ((b * c) + (- (- (q * (s - c))))) is Element of the carrier of PS
(b * c) + (q * (s - c)) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + ((b * c) + (q * (s - c))) is Element of the carrier of PS
(- (a * s)) + (b * c) is Element of the carrier of PS
((a * p) + (- (b * p))) + ((- (a * s)) + (b * c)) is Element of the carrier of PS
(((a * p) + (- (b * p))) + ((- (a * s)) + (b * c))) + (q * (s - c)) is Element of the carrier of PS
((a * p) + (- (b * p))) + (b * c) is Element of the carrier of PS
(- (a * s)) + (q * (s - c)) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (b * c)) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
(- (b * p)) + (b * c) is Element of the carrier of PS
(a * p) + ((- (b * p)) + (b * c)) is Element of the carrier of PS
((a * p) + ((- (b * p)) + (b * c))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
(b * c) - (b * p) is Element of the carrier of PS
(a * p) + ((b * c) - (b * p)) is Element of the carrier of PS
((a * p) + ((b * c) - (b * p))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
(a * p) + (b * (c - p)) is Element of the carrier of PS
((a * p) + (b * (c - p))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
- ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS
(- ((- (a * p)) + (- (b * (c - p))))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
- (- (a * s)) is Element of the carrier of PS
(- (- (a * s))) + (- (q * (s - c))) is Element of the carrier of PS
- ((- (- (a * s))) + (- (q * (s - c)))) is Element of the carrier of PS
(- ((- (a * p)) + (- (b * (c - p))))) + (- ((- (- (a * s))) + (- (q * (s - c))))) is Element of the carrier of PS
(a * s) + (- (q * (s - c))) is Element of the carrier of PS
- ((a * s) + (- (q * (s - c)))) is Element of the carrier of PS
(- ((- (a * p)) + (- (b * (c - p))))) + (- ((a * s) + (- (q * (s - c))))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) + ((a * s) + (- (q * (s - c)))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) + ((a * s) + (- (q * (s - c))))) is Element of the carrier of PS
(- (a * s)) + (- (- (q * (s - c)))) is Element of the carrier of PS
- ((- (a * s)) + (- (- (q * (s - c))))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) + (- ((- (a * s)) + (- (- (q * (s - c)))))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) + (- ((- (a * s)) + (- (- (q * (s - c))))))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (- (q * (s - c))))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (- (q * (s - c)))))) is Element of the carrier of PS
- (s - c) is Element of the carrier of PS
(- (s - c)) * q is Element of the carrier of PS
- ((- (s - c)) * q) is Element of the carrier of PS
(- (a * s)) + (- ((- (s - c)) * q)) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- ((- (s - c)) * q))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- ((- (s - c)) * q)))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (q * (c - s)))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (q * (c - s))))) is Element of the carrier of PS
- (0. PS) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a + b is Element of the carrier of PS
c is Element of the carrier of PS
- c is Element of the carrier of PS
(a + b) + (- c) is Element of the carrier of PS
a - ((a + b) + (- c)) is Element of the carrier of PS
c - b is Element of the carrier of PS
b + (- c) is Element of the carrier of PS
a + (b + (- c)) is Element of the carrier of PS
a - (a + (b + (- c))) is Element of the carrier of PS
b - c is Element of the carrier of PS
a + (b - c) is Element of the carrier of PS
a - (a + (b - c)) is Element of the carrier of PS
- (a + (b - c)) is Element of the carrier of PS
a + (- (a + (b - c))) is Element of the carrier of PS
- a is Element of the carrier of PS
- (b - c) is Element of the carrier of PS
(- a) + (- (b - c)) is Element of the carrier of PS
a + ((- a) + (- (b - c))) is Element of the carrier of PS
a + (- a) is Element of the carrier of PS
(a + (- a)) + (- (b - c)) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
(0. PS) + (- (b - c)) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
- a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c + p is Element of the carrier of PS
q is Element of the carrier of PS
- q is Element of the carrier of PS
(c + p) + (- q) is Element of the carrier of PS
c - ((c + p) + (- q)) is Element of the carrier of PS
(a - b) * (c - ((c + p) + (- q))) is Element of the carrier of PS
q - p is Element of the carrier of PS
s is Element of the carrier of PS
s + b is Element of the carrier of PS
(s + b) + (- a) is Element of the carrier of PS
s - ((s + b) + (- a)) is Element of the carrier of PS
(s - ((s + b) + (- a))) * (q - p) is Element of the carrier of PS
((a - b) * (c - ((c + p) + (- q)))) - ((s - ((s + b) + (- a))) * (q - p)) is Element of the carrier of PS

the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:H1(PS),H1(PS):] is non empty set
[:[:H1(PS),H1(PS):],H1(PS):] is non empty set
bool [:[:H1(PS),H1(PS):],H1(PS):] is non empty set
a is V6() V18([:H1(PS),H1(PS):],H1(PS)) Element of bool [:[:H1(PS),H1(PS):],H1(PS):]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . (b,c) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b `1_3 is Element of the carrier of PS
c `1_3 is Element of the carrier of PS
(b `1_3) + (c `1_3) is Element of the carrier of PS
b `2_3 is Element of the carrier of PS
c `2_3 is Element of the carrier of PS
(b `2_3) + (c `2_3) is Element of the carrier of PS
b `3_3 is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
(b `3_3) + (c `3_3) is Element of the carrier of PS
[((b `1_3) + (c `1_3)),((b `2_3) + (c `2_3)),((b `3_3) + (c `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[:H1(PS),H1(PS):] is non empty set
[:[:H1(PS),H1(PS):],H1(PS):] is non empty set
bool [:[:H1(PS),H1(PS):],H1(PS):] is non empty set
a is V6() V18([:H1(PS),H1(PS):],H1(PS)) Element of bool [:[:H1(PS),H1(PS):],H1(PS):]
b is V6() V18([:H1(PS),H1(PS):],H1(PS)) Element of bool [:[:H1(PS),H1(PS):],H1(PS):]
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . (c,p) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b . (c,p) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c `1_3 is Element of the carrier of PS
p `1_3 is Element of the carrier of PS
(c `1_3) + (p `1_3) is Element of the carrier of PS
c `2_3 is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
(c `2_3) + (p `2_3) is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
(c `3_3) + (p `3_3) is Element of the carrier of PS
[((c `1_3) + (p `1_3)),((c `2_3) + (p `2_3)),((c `3_3) + (p `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) . (a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . (a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a `1_3 is Element of the carrier of PS
b `1_3 is Element of the carrier of PS
(a `1_3) + (b `1_3) is Element of the carrier of PS
a `2_3 is Element of the carrier of PS
b `2_3 is Element of the carrier of PS
(a `2_3) + (b `2_3) is Element of the carrier of PS
a `3_3 is Element of the carrier of PS
b `3_3 is Element of the carrier of PS
(a `3_3) + (b `3_3) is Element of the carrier of PS
[((a `1_3) + (b `1_3)),((a `2_3) + (b `2_3)),((a `3_3) + (b `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
[a,b,c] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
p is Element of the carrier of PS
a + p is Element of the carrier of PS
q is Element of the carrier of PS
b + q is Element of the carrier of PS
s is Element of the carrier of PS
[p,q,s] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,[a,b,c],[p,q,s]) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . ([a,b,c],[p,q,s]) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c + s is Element of the carrier of PS
[(a + p),(b + q),(c + s)] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[a,b,c] `3_3 is Element of the carrier of PS
[p,q,s] `1_3 is Element of the carrier of PS
[p,q,s] `2_3 is Element of the carrier of PS
[p,q,s] `3_3 is Element of the carrier of PS
[a,b,c] `1_3 is Element of the carrier of PS
[a,b,c] `2_3 is Element of the carrier of PS

the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:H1(PS),H1(PS):] is non empty set
bool [:H1(PS),H1(PS):] is non empty set
a is V6() V18(H1(PS),H1(PS)) Element of bool [:H1(PS),H1(PS):]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b `1_3 is Element of the carrier of PS
- (b `1_3) is Element of the carrier of PS
b `2_3 is Element of the carrier of PS
- (b `2_3) is Element of the carrier of PS
b `3_3 is Element of the carrier of PS
- (b `3_3) is Element of the carrier of PS
[(- (b `1_3)),(- (b `2_3)),(- (b `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[:H1(PS),H1(PS):] is non empty set
bool [:H1(PS),H1(PS):] is non empty set
a is V6() V18(H1(PS),H1(PS)) Element of bool [:H1(PS),H1(PS):]
b is V6() V18(H1(PS),H1(PS)) Element of bool [:H1(PS),H1(PS):]
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . c is Element of H1(PS)
b . c is Element of H1(PS)
c `1_3 is Element of the carrier of PS
- (c `1_3) is Element of the carrier of PS
c `2_3 is Element of the carrier of PS
- (c `2_3) is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
- (c `3_3) is Element of the carrier of PS
[(- (c `1_3)),(- (c `2_3)),(- (c `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is V6() V18([: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) . a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]

the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,a) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a `1_3 is Element of the carrier of PS
- (a `1_3) is Element of the carrier of PS
a `2_3 is Element of the carrier of PS
- (a `2_3) is Element of the carrier of PS
a `3_3 is Element of the carrier of PS
- (a `3_3) is Element of the carrier of PS
[(- (a `1_3)),(- (a `2_3)),(- (a `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
PS is set
[:PS,PS,PS,PS:] is set
the non empty set is non empty set
the ( the non empty set ) is ( the non empty set )
( the non empty set , the ( the non empty set )) is () ()
the carrier of ( the non empty set , the ( the non empty set )) is set
PS is non empty ()
the carrier of PS is non empty set

the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set

(PS) is set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set

(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set

(PS) is set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set

(PS) is non empty set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is set
b is set
c is set
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
p `1_3 is Element of the carrier of PS
q `1_3 is Element of the carrier of PS
(p `1_3) - (q `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
(p `3_3) - (q `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
p `1_3 is Element of the carrier of PS
q `1_3 is Element of the carrier of PS
(p `1_3) - (q `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
(p `3_3) - (q `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS

(PS) is set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
a is set
(PS) is non empty set

(PS) is set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set

(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()

(PS) is ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the of (PS) is ( the carrier of (PS))
the carrier of (PS) is non empty set

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set

(q) is non empty () ()
(q) is non empty set
the carrier of q is non empty non trivial set
[: the carrier of q, the carrier of q, the carrier of q:] is non empty set
(q) is ((q))
(q) is set
((q),(q)) is () ()
the carrier of (q) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
s is Element of the carrier of (q)
s is Element of the carrier of (q)
s is Element of the carrier of (q)
c10 is Element of the carrier of (q)
[s,s,s,c10] is Element of [: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):]
[: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):] is non empty set

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set

(q) is non empty () ()
(q) is non empty set
the carrier of q is non empty non trivial set
[: the carrier of q, the carrier of q, the carrier of q:] is non empty set
(q) is ((q))
(q) is set
((q),(q)) is () ()
the carrier of (q) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
s is Element of the carrier of (q)
s is Element of the carrier of (q)
s is Element of the carrier of (q)
c10 is Element of the carrier of (q)
[s,s,s,c10] is Element of [: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):]
[: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):] is non empty set
(q) is non empty set
[:(q),(q),(q),(q):] is non empty set
h is Element of [: the carrier of q, the carrier of q, the carrier of q:]
i is Element of [: the carrier of q, the carrier of q, the carrier of q:]
j is Element of [: the carrier of q, the carrier of q, the carrier of q:]
k is Element of [: the carrier of q, the carrier of q, the carrier of q:]
[h,i,j,k] is Element of [:[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:]:]
[:[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:]:] is non empty set
h `1_3 is Element of the carrier of q
i `1_3 is Element of the carrier of q
(h `1_3) - (i `1_3) is Element of the carrier of q
j `2_3 is Element of the carrier of q
k `2_3 is Element of the carrier of q
(j `2_3) - (k `2_3) is Element of the carrier of q
((h `1_3) - (i `1_3)) * ((j `2_3) - (k `2_3)) is Element of the carrier of q
j `1_3 is Element of the carrier of q
k `1_3 is Element of the carrier of q
(j `1_3) - (k `1_3) is Element of the carrier of q
h `2_3 is Element of the carrier of q
i `2_3 is Element of the carrier of q
(h `2_3) - (i `2_3) is Element of the carrier of q
((j `1_3) - (k `1_3)) * ((h `2_3) - (i `2_3)) is Element of the carrier of q
(((h `1_3) - (i `1_3)) * ((j `2_3) - (k `2_3))) - (((j `1_3) - (k `1_3)) * ((h `2_3) - (i `2_3))) is Element of the carrier of q
0. q is V49(q) Element of the carrier of q
the ZeroF of q is Element of the carrier of q
j `3_3 is Element of the carrier of q
k `3_3 is Element of the carrier of q
(j `3_3) - (k `3_3) is Element of the carrier of q
((h `1_3) - (i `1_3)) * ((j `3_3) - (k `3_3)) is Element of the carrier of q
h `3_3 is Element of the carrier of q
i `3_3 is Element of the carrier of q
(h `3_3) - (i `3_3) is Element of the carrier of q
((j `1_3) - (k `1_3)) * ((h `3_3) - (i `3_3)) is Element of the carrier of q
(((h `1_3) - (i `1_3)) * ((j `3_3) - (k `3_3))) - (((j `1_3) - (k `1_3)) * ((h `3_3) - (i `3_3))) is Element of the carrier of q
((h `2_3) - (i `2_3)) * ((j `3_3) - (k `3_3)) is Element of the carrier of q
((j `2_3) - (k `2_3)) * ((h `3_3) - (i `3_3)) is Element of the carrier of q
(((h `2_3) - (i `2_3)) * ((j `3_3) - (k `3_3))) - (((j `2_3) - (k `2_3)) * ((h `3_3) - (i `3_3))) is Element of the carrier of q

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[q,s,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
q `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(q `1_3) - (s `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(q `2_3) - (s `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(q `3_3) - (s `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS
((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[q,s,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
q `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(q `1_3) - (s `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(q `2_3) - (s `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(q `3_3) - (s `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS
((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
[a,b,b,a] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[c,p,p,c] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
c `2_3 is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
(c `2_3) - (p `2_3) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
(p `3_3) - (c `3_3) is Element of the carrier of PS
((c `2_3) - (p `2_3)) * ((p `3_3) - (c `3_3)) is Element of the carrier of PS
(p `2_3) - (c `2_3) is Element of the carrier of PS
(c `3_3) - (p `3_3) is Element of the carrier of PS
((p `2_3) - (c `2_3)) * ((c `3_3) - (p `3_3)) is Element of the carrier of PS
(((c `2_3) - (p `2_3)) * ((p `3_3) - (c `3_3))) - (((p `2_3) - (c `2_3)) * ((c `3_3) - (p `3_3))) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
c `1_3 is Element of the carrier of PS
p `1_3 is Element of the carrier of PS
(c `1_3) - (p `1_3) is Element of the carrier of PS
((c `1_3) - (p `1_3)) * ((p `2_3) - (c `2_3)) is Element of the carrier of PS
(p `1_3) - (c `1_3) is Element of the carrier of PS
((p `1_3) - (c `1_3)) * ((c `2_3) - (p `2_3)) is Element of the carrier of PS
(((c `1_3) - (p `1_3)) * ((p `2_3) - (c `2_3))) - (((p `1_3) - (c `1_3)) * ((c `2_3) - (p `2_3))) is Element of the carrier of PS
((c `1_3) - (p `1_3)) * ((p `3_3) - (c `3_3)) is Element of the carrier of PS
((p `1_3) - (c `1_3)) * ((c `3_3) - (p `3_3)) is Element of the carrier of PS
(((c `1_3) - (p `1_3)) * ((p `3_3) - (c `3_3))) - (((p `1_3) - (c `1_3)) * ((c `3_3) - (p `3_3))) is Element of the carrier of PS

(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
[a,b,c,c] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
p `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((p `2_3) - (q `2_3))