let CPS be CollProjectiveSpace; ( ( for p1, r2, q, r1, q1, p, r being Point of CPS st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds
r2,r1,q1 are_collinear ) implies for p, q, r, s, a, b, c being POINT of (IncProjSp_of CPS)
for L, Q, R, S, A, B, C being LINE of (IncProjSp_of CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C )
assume A1:
for p1, r2, q, r1, q1, p, r being Element of CPS st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds
r2,r1,q1 are_collinear
; for p, q, r, s, a, b, c being POINT of (IncProjSp_of CPS)
for L, Q, R, S, A, B, C being LINE of (IncProjSp_of CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C
let p, q, r, s, a, b, c be POINT of (IncProjSp_of CPS); for L, Q, R, S, A, B, C being LINE of (IncProjSp_of CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C
let L, Q, R, S, A, B, C be LINE of (IncProjSp_of CPS); ( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C implies not c on C )
assume that
A2:
not q on L
and
A3:
not r on L
and
A4:
not p on Q
and
A5:
not s on Q
and
A6:
not p on R
and
A7:
not r on R
and
A8:
{a,p,s} on L
and
A9:
{a,q,r} on Q
and
A10:
{b,q,s} on R
and
A11:
{b,p,r} on S
and
A12:
{c,p,q} on A
and
A13:
{c,r,s} on B
and
A14:
{a,b} on C
; not c on C
reconsider p9 = p, q9 = q, r9 = r, s9 = s, a9 = a, b9 = b, c9 = c as Point of CPS ;
A15:
( p on L & s on L )
by A8, INCSP_1:2;
A16:
s on R
by A10, INCSP_1:2;
A17:
now ( p9,r9,s9 are_collinear implies ( s on S & contradiction ) )assume
p9,
r9,
s9 are_collinear
;
( s on S & contradiction )then A18:
ex
K being
LINE of
(IncProjSp_of CPS) st
(
p on K &
r on K &
s on K )
by Th10;
hence
s on S
by A3, A6, A15, A16, Th8;
contradictionthus
contradiction
by A3, A6, A15, A16, A18, Th8;
verum end;
A19:
now ( p9,s9,q9 are_collinear implies ( p on R & contradiction ) )assume
p9,
s9,
q9 are_collinear
;
( p on R & contradiction )then A20:
ex
K being
LINE of
(IncProjSp_of CPS) st
(
p on K &
s on K &
q on K )
by Th10;
hence
p on R
by A2, A15, A16, Th8;
contradictionthus
contradiction
by A2, A6, A15, A16, A20, Th8;
verum end;
a on L
by A8, INCSP_1:2;
then A21:
p9,s9,a9 are_collinear
by A15, Th10;
assume A22:
c on C
; contradiction
( a on C & b on C )
by A14, INCSP_1:1;
then A23:
a9,b9,c9 are_collinear
by A22, Th10;
A24:
( q on Q & r on Q )
by A9, INCSP_1:2;
A25:
q on R
by A10, INCSP_1:2;
A26:
now ( p9,r9,q9 are_collinear implies ( q on S & contradiction ) )assume
p9,
r9,
q9 are_collinear
;
( q on S & contradiction )then A27:
ex
K being
LINE of
(IncProjSp_of CPS) st
(
p on K &
r on K &
q on K )
by Th10;
hence
q on S
by A4, A7, A24, A25, Th8;
contradictionthus
contradiction
by A4, A7, A24, A25, A27, Th8;
verum end;
A28:
now ( r9,s9,q9 are_collinear implies ( r on R & contradiction ) )assume
r9,
s9,
q9 are_collinear
;
( r on R & contradiction )then A29:
ex
K being
LINE of
(IncProjSp_of CPS) st
(
r on K &
s on K &
q on K )
by Th10;
hence
r on R
by A5, A24, A25, Th8;
contradictionthus
contradiction
by A5, A7, A24, A25, A29, Th8;
verum end;
a on Q
by A9, INCSP_1:2;
then A30:
r9,q9,a9 are_collinear
by A24, Th10;
A31:
r on S
by A11, INCSP_1:2;
( b on S & p on S )
by A11, INCSP_1:2;
then A32:
p9,r9,b9 are_collinear
by A31, Th10;
A33:
s on B
by A13, INCSP_1:2;
( c on B & r on B )
by A13, INCSP_1:2;
then A34:
r9,s9,c9 are_collinear
by A33, Th10;
A35:
q on A
by A12, INCSP_1:2;
( c on A & p on A )
by A12, INCSP_1:2;
then A36:
p9,q9,c9 are_collinear
by A35, Th10;
b on R
by A10, INCSP_1:2;
then
s9,q9,b9 are_collinear
by A25, A16, Th10;
hence
contradiction
by A1, A23, A32, A21, A30, A36, A34, A26, A17, A19, A28; verum