theorem Th18:
for
a,
b,
c,
d,
e,
f being
Element of
F_Real holds
( (
qfconic (
a,
b,
c,
d,
e,
f,
|[1,0,0]|)
= 0 implies
a = 0 ) & (
qfconic (
a,
b,
c,
d,
e,
f,
|[0,1,0]|)
= 0 implies
b = 0 ) & (
qfconic (
a,
b,
c,
d,
e,
f,
|[0,0,1]|)
= 0 implies
c = 0 ) & (
qfconic (
0,
0,
0,
d,
e,
f,
|[1,1,1]|)
= 0 implies
(d + e) + f = 0 ) )