theorem Th18:
for
CPS being
CollProjectiveSpace st ( for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Point of
CPS st
o <> q1 &
p1 <> q1 &
o <> q2 &
p2 <> q2 &
o <> q3 &
p3 <> q3 & not
o,
p1,
p2 are_collinear & not
o,
p1,
p3 are_collinear & not
o,
p2,
p3 are_collinear &
p1,
p2,
r3 are_collinear &
q1,
q2,
r3 are_collinear &
p2,
p3,
r1 are_collinear &
q2,
q3,
r1 are_collinear &
p1,
p3,
r2 are_collinear &
q1,
q3,
r2 are_collinear &
o,
p1,
q1 are_collinear &
o,
p2,
q2 are_collinear &
o,
p3,
q3 are_collinear holds
r1,
r2,
r3 are_collinear ) holds
for
o,
b1,
a1,
b2,
a2,
b3,
a3,
r,
s,
t being
POINT of
(IncProjSp_of CPS) for
C1,
C2,
C3,
A1,
A2,
A3,
B1,
B2,
B3 being
LINE of
(IncProjSp_of CPS) st
{o,b1,a1} on C1 &
{o,a2,b2} on C2 &
{o,a3,b3} on C3 &
{a3,a2,t} on A1 &
{a3,r,a1} on A2 &
{a2,s,a1} on A3 &
{t,b2,b3} on B1 &
{b1,r,b3} on B2 &
{b1,s,b2} on B3 &
C1,
C2,
C3 are_mutually_distinct &
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 &
a1 <> b1 &
a2 <> b2 &
a3 <> b3 holds
ex
O being
LINE of
(IncProjSp_of CPS) st
{r,s,t} on O