let CPS be CollProjectiveSpace; :: thesis: ( ( for p1, r2, q, r1, q1, p, r being Point of 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
for L, Q, R, S, A, B, C being LINE of 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 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
for L, Q, R, S, A, B, C being LINE of 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 ; :: thesis: for L, Q, R, S, A, B, C being LINE of 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 ; :: 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 p' = p, q' = q, r' = r, s' = s, a' = a, b' = b, c' = c as Point of ;
A15: ( p on L & s on L ) by A8, INCSP_1:12;
A16: s on R by A10, INCSP_1:12;

A17: now

assume p',r',s' is_collinear ; :: thesis: ( s on S & contradiction )
then A18: ex K being LINE of st
( p on K & r on K & s on K ) by Th14;
hence s on S by A3, A6, A15, A16, Th12; :: thesis: contradiction
thus contradiction by A3, A6, A15, A16, A18, Th12; :: thesis: verum

end;

A19: now

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

end;

a on L by A8, INCSP_1:12;
then A21: p',s',a' is_collinear by A15, Th14;
assume A22: c on C ; :: thesis: contradiction
( a on C & b on C ) by A14, INCSP_1:11;
then A23: a',b',c' is_collinear by A22, Th14;
A24: ( q on Q & r on Q ) by A9, INCSP_1:12;
A25: q on R by A10, INCSP_1:12;

A26: now

assume p',r',q' is_collinear ; :: thesis: ( q on S & contradiction )
then A27: ex K being LINE of st
( p on K & r on K & q on K ) by Th14;
hence q on S by A4, A7, A24, A25, Th12; :: thesis: contradiction
thus contradiction by A4, A7, A24, A25, A27, Th12; :: thesis: verum

end;

A28: now

assume r',s',q' is_collinear ; :: thesis: ( r on R & contradiction )
then A29: ex K being LINE of st
( r on K & s on K & q on K ) by Th14;
hence r on R by A5, A24, A25, Th12; :: thesis: contradiction
thus contradiction by A5, A7, A24, A25, A29, Th12; :: thesis: verum

end;

a on Q by A9, INCSP_1:12;
then A30: r',q',a' is_collinear by A24, Th14;
A31: r on S by A11, INCSP_1:12;
( b on S & p on S ) by A11, INCSP_1:12;
then A32: p',r',b' is_collinear by A31, Th14;
A33: s on B by A13, INCSP_1:12;
( c on B & r on B ) by A13, INCSP_1:12;
then A34: r',s',c' is_collinear by A33, Th14;
A35: q on A by A12, INCSP_1:12;
( c on A & p on A ) by A12, INCSP_1:12;
then A36: p',q',c' is_collinear by A35, Th14;
b on R by A10, INCSP_1:12;
then s',q',b' is_collinear by A25, A16, Th14;
hence contradiction by A1, A23, A32, A21, A30, A36, A34, A26, A17, A19, A28; :: thesis: verum