let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
let a, b be POINT of IPP; :: thesis: for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
let A, B, C, Q, O be LINE of IPP; :: thesis: ( not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O implies ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) ) )
assume that
A1: not a on A and
A2: not b on B and
A3: not a on C and
A4: not b on C and
A5: not A,B,C are_concurrent and
A6: B,C,Q are_concurrent and
A7: not a on Q and
A8: ( B <> Q & a <> b & a on O & b on O ) ; :: thesis: ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
A9: ( IncProj B,b,C is one-to-one & IncProj C,a,A is one-to-one ) by A1, A2, A3, A4, Th8;
not B,A,C are_concurrent

proof

assume B,A,C are_concurrent ; :: thesis: contradiction
then ex o being POINT of IPP st
( o on B & o on A & o on C ) by Def1;
hence contradiction by A5, Def1; :: thesis: verum

end;

then consider q being POINT of IPP such that
A10: q on O and
A11: ( not q on B & not q on Q ) and
A12: (IncProj C,a,A) * (IncProj B,b,C) = (IncProj Q,a,A) * (IncProj B,q,Q) by A1, A2, A3, A4, A6, A7, A8, Th21;
take q ; :: thesis: ( q on O & not q on B & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
thus ( q on O & not q on B & not q on Q ) by A10, A11; :: thesis: (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q)
A13: IncProj B,q,Q is one-to-one by A11, Th8;
A14: IncProj Q,a,A is one-to-one by A1, A7, Th8;
thus (IncProj C,b,B) * (IncProj A,a,C) = ((IncProj B,b,C) " ) * (IncProj A,a,C) by A2, A4, Th9
.= ((IncProj B,b,C) " ) * ((IncProj C,a,A) " ) by A1, A3, Th9
.= ((IncProj Q,a,A) * (IncProj B,q,Q)) " by A12, A9, FUNCT_1:66
.= ((IncProj B,q,Q) " ) * ((IncProj Q,a,A) " ) by A13, A14, FUNCT_1:66
.= (IncProj Q,q,B) * ((IncProj Q,a,A) " ) by A11, Th9
.= (IncProj Q,q,B) * (IncProj A,a,Q) by A1, A7, Th9 ; :: thesis: verum