theorem Th17:
for
a,
b,
c,
d,
e,
f being
Real for
P1,
P2,
P3,
P4,
P5,
P6 being
Point of
(ProjectiveSpace (TOP-REAL 3)) for
N being
invertible Matrix of 3,
F_Real st ( not
a = 0 or not
b = 0 or not
c = 0 or not
d = 0 or not
e = 0 or not
f = 0 ) &
P1 in conic (
a,
b,
c,
d,
e,
f) &
P2 in conic (
a,
b,
c,
d,
e,
f) &
P3 in conic (
a,
b,
c,
d,
e,
f) &
P4 in conic (
a,
b,
c,
d,
e,
f) &
P5 in conic (
a,
b,
c,
d,
e,
f) &
P6 in conic (
a,
b,
c,
d,
e,
f) holds
ex
a2,
b2,
c2,
d2,
e2,
f2 being
Real st
( ( not
a2 = 0 or not
b2 = 0 or not
c2 = 0 or not
d2 = 0 or not
e2 = 0 or not
f2 = 0 ) &
(homography N) . P1 in conic (
a2,
b2,
c2,
d2,
e2,
f2) &
(homography N) . P2 in conic (
a2,
b2,
c2,
d2,
e2,
f2) &
(homography N) . P3 in conic (
a2,
b2,
c2,
d2,
e2,
f2) &
(homography N) . P4 in conic (
a2,
b2,
c2,
d2,
e2,
f2) &
(homography N) . P5 in conic (
a2,
b2,
c2,
d2,
e2,
f2) &
(homography N) . P6 in conic (
a2,
b2,
c2,
d2,
e2,
f2) )