let CPS be CollProjectiveSpace; ( ( 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 ) implies 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 )
assume A1:
for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element 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
; 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
let o, b1, a1, b2, a2, b3, a3, r, s, t be 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
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of (IncProjSp_of CPS); ( {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 implies ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O )
assume that
A2:
{o,b1,a1} on C1
and
A3:
{o,a2,b2} on C2
and
A4:
{o,a3,b3} on C3
and
A5:
{a3,a2,t} on A1
and
A6:
{a3,r,a1} on A2
and
A7:
{a2,s,a1} on A3
and
A8:
{t,b2,b3} on B1
and
A9:
{b1,r,b3} on B2
and
A10:
{b1,s,b2} on B3
and
A11:
C1,C2,C3 are_mutually_distinct
and
A12:
( o <> a1 & o <> a2 & o <> a3 )
and
A13:
o <> b1
and
A14:
o <> b2
and
A15:
o <> b3
and
A16:
( a1 <> b1 & a2 <> b2 & a3 <> b3 )
; ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O
reconsider o9 = o, b19 = b1, a19 = a1, b29 = b2, a29 = a2, b39 = b3, a39 = a3, r9 = r, s9 = s, t9 = t as Element of CPS ;
A17:
( o on C2 & b2 on C2 )
by A3, INCSP_1:2;
A18:
s on B3
by A10, INCSP_1:2;
( b2 on B3 & b1 on B3 )
by A10, INCSP_1:2;
then A19:
b19,b29,s9 are_collinear
by A18, Th10;
A20:
r on B2
by A9, INCSP_1:2;
( b3 on B2 & b1 on B2 )
by A9, INCSP_1:2;
then A21:
b19,b39,r9 are_collinear
by A20, Th10;
A22:
t on B1
by A8, INCSP_1:2;
( b3 on B1 & b2 on B1 )
by A8, INCSP_1:2;
then A23:
b29,b39,t9 are_collinear
by A22, Th10;
A24:
s on A3
by A7, INCSP_1:2;
( a2 on A3 & a1 on A3 )
by A7, INCSP_1:2;
then A25:
a19,a29,s9 are_collinear
by A24, Th10;
A26:
( o on C3 & b3 on C3 )
by A4, INCSP_1:2;
a3 on C3
by A4, INCSP_1:2;
then A27:
o9,b39,a39 are_collinear
by A26, Th10;
a2 on C2
by A3, INCSP_1:2;
then A28:
o9,b29,a29 are_collinear
by A17, Th10;
A29:
r on A2
by A6, INCSP_1:2;
( a3 on A2 & a1 on A2 )
by A6, INCSP_1:2;
then A30:
a19,a39,r9 are_collinear
by A29, Th10;
A31:
t on A1
by A5, INCSP_1:2;
( a3 on A1 & a2 on A1 )
by A5, INCSP_1:2;
then A32:
a29,a39,t9 are_collinear
by A31, Th10;
A33:
( o on C1 & b1 on C1 )
by A2, INCSP_1:2;
A34:
( not o9,b19,b29 are_collinear & not o9,b19,b39 are_collinear & not o9,b29,b39 are_collinear )
a1 on C1
by A2, INCSP_1:2;
then
o9,b19,a19 are_collinear
by A33, Th10;
then
t9,r9,s9 are_collinear
by A1, A12, A16, A19, A25, A21, A30, A23, A32, A28, A27, A34;
then consider O being LINE of (IncProjSp_of CPS) such that
A41:
( t on O & r on O & s on O )
by Th10;
{r,s,t} on O
by A41, INCSP_1:2;
hence
ex O being LINE of (IncProjSp_of CPS) st {r,s,t} on O
; verum