let CPS be CollProjectiveSpace; ( ( 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 ) implies 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 )
assume A1:
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
; 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
let o, a1, a2, a3, b1, b2, b3, c1, c2, c3 be 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
let A1, A2, A3, B1, B2, B3, C1, C2, C3 be LINE of (IncProjSp_of CPS); ( 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 implies c3 on C3 )
assume that
A2:
o,a1,a2,a3 are_mutually_distinct
and
A3:
o,b1,b2,b3 are_mutually_distinct
and
A4:
A3 <> B3
and
A5:
o on A3
and
A6:
o on B3
and
A7:
{a2,b3,c1} on A1
and
A8:
{a3,b1,c2} on B1
and
A9:
{a1,b2,c3} on C1
and
A10:
{a1,b3,c2} on A2
and
A11:
{a3,b2,c1} on B2
and
A12:
{a2,b1,c3} on C2
and
A13:
{b1,b2,b3} on A3
and
A14:
{a1,a2,a3} on B3
and
A15:
{c1,c2} on C3
; c3 on C3
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3, c19 = c1, c29 = c2, c39 = c3 as Point of CPS ;
A16:
b1 on A3
by A13, INCSP_1:2;
A17:
c3 on C1
by A9, INCSP_1:2;
( a1 on C1 & b2 on C1 )
by A9, INCSP_1:2;
then A18:
a19,b29,c39 are_collinear
by A17, Th10;
A19:
c1 on A1
by A7, INCSP_1:2;
A20:
( o9 <> b39 & b29 <> b39 )
by A3, ZFMISC_1:def 6;
A21:
( a29 <> a39 & a19 <> a29 )
by A2, ZFMISC_1:def 6;
A22:
( b3 on A2 & c2 on A2 )
by A10, INCSP_1:2;
A23:
a1 on A2
by A10, INCSP_1:2;
then A24:
a19,b39,c29 are_collinear
by A22, Th10;
A25:
( b19 <> b29 & b19 <> b39 )
by A3, ZFMISC_1:def 6;
A26:
b3 on A1
by A7, INCSP_1:2;
A27:
a1 on B3
by A14, INCSP_1:2;
A28:
not o9,a19,b19 are_collinear
proof
A29:
o <> a1
by A2, ZFMISC_1:def 6;
assume
o9,
a19,
b19 are_collinear
;
contradiction
then consider K being
LINE of
(IncProjSp_of CPS) such that A30:
o on K
and A31:
a1 on K
and A32:
b1 on K
by Th10;
o <> b1
by A3, ZFMISC_1:def 6;
then
K = A3
by A5, A16, A30, A32, Th8;
hence
contradiction
by A4, A6, A27, A30, A31, A29, Th8;
verum
end;
A33:
c3 on C2
by A12, INCSP_1:2;
( a2 on C2 & b1 on C2 )
by A12, INCSP_1:2;
then A34:
b19,a29,c39 are_collinear
by A33, Th10;
A35:
a3 on B1
by A8, INCSP_1:2;
A36:
b2 on A3
by A13, INCSP_1:2;
then A37:
o9,b19,b29 are_collinear
by A5, A16, Th10;
A38:
( a3 on B2 & c1 on B2 )
by A11, INCSP_1:2;
A39:
b2 on B2
by A11, INCSP_1:2;
then A40:
a39,b29,c19 are_collinear
by A38, Th10;
A41:
b3 on A3
by A13, INCSP_1:2;
then A42:
o9,b19,b39 are_collinear
by A5, A16, Th10;
A43:
( a19 <> a39 & o9 <> b29 )
by A2, A3, ZFMISC_1:def 6;
A44:
( o9 <> a29 & o9 <> a39 )
by A2, ZFMISC_1:def 6;
A45:
c2 on B1
by A8, INCSP_1:2;
A46:
a2 on A1
by A7, INCSP_1:2;
then A47:
a29,b39,c19 are_collinear
by A26, A19, Th10;
A48:
b1 <> b2
by A3, ZFMISC_1:def 6;
A49:
a1 <> a2
by A2, ZFMISC_1:def 6;
A50:
o <> b3
by A3, ZFMISC_1:def 6;
A51:
b1 on B1
by A8, INCSP_1:2;
then A52:
a39,b19,c29 are_collinear
by A35, A45, Th10;
A53:
a3 on B3
by A14, INCSP_1:2;
then A54:
o9,a19,a39 are_collinear
by A6, A27, Th10;
A55:
a2 on B3
by A14, INCSP_1:2;
then
o9,a19,a29 are_collinear
by A6, A27, Th10;
then
c19,c29,c39 are_collinear
by A1, A44, A21, A43, A20, A25, A28, A54, A37, A42, A18, A34, A24, A52, A47, A40;
then A56:
ex K being LINE of (IncProjSp_of CPS) st
( c1 on K & c2 on K & c3 on K )
by Th10;
A57:
o <> a3
by A2, ZFMISC_1:def 6;
A58:
c1 <> c2
proof
assume A59:
not
c1 <> c2
;
contradiction
not
a3 on A3
by A4, A5, A6, A57, A53, Th8;
then
B1 <> B2
by A48, A35, A51, A39, A16, A36, Th8;
then A60:
c1 = a3
by A35, A45, A38, A59, Th8;
not
b3 on B3
by A4, A5, A6, A50, A41, Th8;
then
A1 <> A2
by A49, A46, A26, A23, A27, A55, Th8;
then
c1 = b3
by A26, A19, A22, A59, Th8;
hence
contradiction
by A4, A5, A6, A50, A41, A53, A60, Th8;
verum
end;
( c1 on C3 & c2 on C3 )
by A15, INCSP_1:1;
hence
c3 on C3
by A58, A56, Th8; verum