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