let CPS be CollProjectiveSpace; :: thesis: ( ( 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 ; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 :: thesis: ( p9,r9,s9 are_collinear implies ( s on S & contradiction ) )
assume p9,r9,s9 are_collinear ; :: thesis: ( 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; :: thesis: contradiction
thus contradiction by A3, A6, A15, A16, A18, Th8; :: thesis: verum
end;
A19: now :: thesis: ( p9,s9,q9 are_collinear implies ( p on R & contradiction ) )
assume p9,s9,q9 are_collinear ; :: thesis: ( 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; :: thesis: contradiction
thus contradiction by A2, A6, A15, A16, A20, Th8; :: thesis: 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 ; :: thesis: 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 :: thesis: ( p9,r9,q9 are_collinear implies ( q on S & contradiction ) )
assume p9,r9,q9 are_collinear ; :: thesis: ( 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; :: thesis: contradiction
thus contradiction by A4, A7, A24, A25, A27, Th8; :: thesis: verum
end;
A28: now :: thesis: ( r9,s9,q9 are_collinear implies ( r on R & contradiction ) )
assume r9,s9,q9 are_collinear ; :: thesis: ( 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; :: thesis: contradiction
thus contradiction by A5, A7, A24, A25, A29, Th8; :: thesis: 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; :: thesis: verum