let CPS be CollProjectiveSpace; :: thesis: ( ( for p1, r2, q, r1, q1, p, r being Point of CPS st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_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 & not q on S & not s on S & {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 is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_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 & not q on S & not s on S & {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 & not q on S & not s on S & {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 & not q on S & not s on S & {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 & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S ) and
A3: ( {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 ) ; :: thesis: not c on C
assume A4: c on C ; :: thesis: contradiction
reconsider p' = p, q' = q, r' = r, s' = s, a' = a, b' = b, c' = c as Point of CPS ;
( a on C & b on C ) by A3, INCSP_1:11;
then A5: a',b',c' is_collinear by A4, Th14;
A6: ( a on L & p on L & s on L & a on Q & q on Q & r on Q & b on R & q on R & s on R & b on S & p on S & r on S & c on A & p on A & q on A & c on B & r on B & s on B ) by A3, INCSP_1:12;
then A7: ( p',r',b' is_collinear & s',q',b' is_collinear & p',s',a' is_collinear & r',q',a' is_collinear & p',q',c' is_collinear & r',s',c' is_collinear ) by Th14;

A8: now

assume p',r',q' is_collinear ; :: thesis: ( q on S & contradiction )
then A9: ex K being LINE of (IncProjSp_of CPS) st
( p on K & r on K & q on K ) by Th14;
hence q on S by A2, A6, Th12; :: thesis: contradiction
thus contradiction by A2, A6, A9, Th12; :: thesis: verum

end;

A10: now

assume p',r',s' is_collinear ; :: thesis: ( s on S & contradiction )
then A11: ex K being LINE of (IncProjSp_of CPS) st
( p on K & r on K & s on K ) by Th14;
hence s on S by A2, A6, Th12; :: thesis: contradiction
thus contradiction by A2, A6, A11, Th12; :: thesis: verum

end;

A12: now

assume p',s',q' is_collinear ; :: thesis: ( p on R & contradiction )
then A13: ex K being LINE of (IncProjSp_of CPS) st
( p on K & s on K & q on K ) by Th14;
hence p on R by A2, A6, Th12; :: thesis: contradiction
thus contradiction by A2, A6, A13, Th12; :: thesis: verum

end;

now

assume r',s',q' is_collinear ; :: thesis: ( r on R & contradiction )
then A14: ex K being LINE of (IncProjSp_of CPS) st
( r on K & s on K & q on K ) by Th14;
hence r on R by A2, A6, Th12; :: thesis: contradiction
thus contradiction by A2, A6, A14, Th12; :: thesis: verum

end;

hence contradiction by A1, A5, A7, A8, A10, A12; :: thesis: verum