let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let a, b, c, d, s, r be POINT of IPP; :: thesis:
let A, B, C, S, R, Q be LINE of IPP; :: thesis:
assume A1: ( not a on A & not b on B & not a on C & not b on C & not a on B & not b on A & c on A & c on C & d on B & d on C & a on S & d on S & c on R & b on R & s on A & s on S & r on B & r on R & s on Q & r on Q & not A,B,C are_concurrent ) ; :: thesis:
then A2: ( A <> B & A <> C & C <> B ) by Th1;
A3: ( c <> d & c <> s & d <> r & c <> b & a <> d )

proof

thus A4: c <> d by A1, Def1; :: thesis:
hence c <> s by A1, INCPROJ:def 9; :: thesis:
thus d <> r by A1, A4, INCPROJ:def 9; :: thesis:
thus ( c <> b & a <> d ) by A1; :: thesis:

end;

A5: C,A,R are_mutually_different by A1, A2, ZFMISC_1:def 5;
A6: ( not a on Q & not b on Q )

proof

A7: now

assume a on Q ; :: thesis:
then S = Q by A1, INCPROJ:def 9;
hence contradiction by A1, A3, INCPROJ:def 9; :: thesis:

end;

now

assume b on Q ; :: thesis:
then R = Q by A1, INCPROJ:def 9;
hence contradiction by A1, A3, INCPROJ:def 9; :: thesis:

end;

hence ( not a on Q & not b on Q ) by A7; :: thesis:

end;

set f = IncProj A,a,C;
set g = IncProj C,b,B;
set g1 = IncProj Q,a,B;
set f1 = IncProj A,b,Q;
A8: ( dom (IncProj A,a,C) = CHAIN A & dom (IncProj C,b,B) = CHAIN C & dom (IncProj A,b,Q) = CHAIN A & dom (IncProj Q,a,B) = CHAIN Q ) by A1, A6, Th5;
A9: for x being POINT of IPP st x on A holds
((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,a,B) * (IncProj A,b,Q)) . x

proof

let x be POINT of IPP; :: thesis:
assume A10: x on A ; :: thesis:
then reconsider x' = (IncProj A,a,C) . x, y = (IncProj A,b,Q) . x as POINT of IPP by A1, A6, PROJRED1:22;
A11: ( x' on C & y on Q ) by A1, A6, A10, PROJRED1:23;
then reconsider x'' = (IncProj C,b,B) . x' as POINT of IPP by A1, PROJRED1:22;
A12: x'' on B by A1, A11, PROJRED1:23;
consider O1 being LINE of IPP such that
A13: ( a on O1 & x on O1 & x' on O1 ) by A1, A10, A11, PROJRED1:def 1;
consider O2 being LINE of IPP such that
A14: ( b on O2 & x' on O2 & x'' on O2 ) by A1, A11, A12, PROJRED1:def 1;
consider O3 being LINE of IPP such that
A15: ( b on O3 & x on O3 & y on O3 ) by A1, A6, A10, A11, PROJRED1:def 1;

A16: now

assume A17: s = x ; :: thesis:
then x' = d by A1, PROJRED1:def 1;
then A18: x'' = d by A1, PROJRED1:27;
y = s by A1, A6, A17, PROJRED1:27;
hence (IncProj C,b,B) . ((IncProj A,a,C) . x) = (IncProj Q,a,B) . ((IncProj A,b,Q) . x) by A1, A6, A18, PROJRED1:def 1; :: thesis:

end;

A19: now

assume A20: s <> x ; :: thesis:
A21: ( {c,d,x'} on C & {c,x,s} on A & {c,b,r} on R ) by A1, A10, A11, INCSP_1:12;
( {b,x,y} on O3 & {b,x'',x'} on O2 & {x,a,x'} on O1 & {y,s,r} on Q & {d,x'',r} on B & {d,a,s} on S ) by A1, A11, A12, A13, A14, A15, INCSP_1:12;
then consider O4 being LINE of IPP such that
A22: {x'',a,y} on O4 by A3, A5, A20, A21, PROJRED1:14;
( x'' on O4 & a on O4 & y on O4 ) by A22, INCSP_1:12;
hence (IncProj C,b,B) . ((IncProj A,a,C) . x) = (IncProj Q,a,B) . ((IncProj A,b,Q) . x) by A1, A6, A11, A12, PROJRED1:def 1; :: thesis:

end;

A23: ( x in dom (IncProj A,a,C) & x' in dom (IncProj C,b,B) & y in dom (IncProj Q,a,B) & x in dom (IncProj A,b,Q) ) by A8, A10, A11;
then ((IncProj C,b,B) * (IncProj A,a,C)) . x = (IncProj Q,a,B) . ((IncProj A,b,Q) . x) by A16, A19, FUNCT_1:23
.= ((IncProj Q,a,B) * (IncProj A,b,Q)) . x by A23, FUNCT_1:23 ;
hence ((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,a,B) * (IncProj A,b,Q)) . x ; :: thesis:

end;

set X = CHAIN A;
A24: ( dom ((IncProj C,b,B) * (IncProj A,a,C)) = CHAIN A & dom ((IncProj Q,a,B) * (IncProj A,b,Q)) = CHAIN A ) by A1, A6, A8, PROJRED1:25;

now

let y be set ; :: thesis:
assume y in CHAIN A ; :: thesis:
then ex x being POINT of IPP st
( y = x & x on A ) ;
hence ((IncProj C,b,B) * (IncProj A,a,C)) . y = ((IncProj Q,a,B) * (IncProj A,b,Q)) . y by A9; :: thesis:

end;

hence (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,a,B) * (IncProj A,b,Q) by A24, FUNCT_1:9; :: thesis: