theorem Th28:
for
e1,
e2,
e3,
f1,
f2,
f3 being
Element of
F_Real for
r1,
r2 being
Real for
p1,
p2,
p3,
p4,
p5,
p6 being
Point of
(TOP-REAL 3) st
p1 = <*1,0,0*> &
p2 = <*0,1,0*> &
p3 = <*0,0,1*> &
p4 = <*1,1,1*> &
p5 = <*e1,e2,e3*> &
p6 = <*f1,f2,f3*> &
qfconic (
0,
0,
0,
r1,
r2,
(- (r1 + r2)),
p5)
= 0 &
qfconic (
0,
0,
0,
r1,
r2,
(- (r1 + r2)),
p6)
= 0 holds
(
qfconic (
0,
0,
0,
r1,
r2,
(- (r1 + r2)),
p1)
= 0 &
qfconic (
0,
0,
0,
r1,
r2,
(- (r1 + r2)),
p2)
= 0 &
qfconic (
0,
0,
0,
r1,
r2,
(- (r1 + r2)),
p3)
= 0 &
qfconic (
0,
0,
0,
r1,
r2,
(- (r1 + r2)),
p4)
= 0 &
((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 &
((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )