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 A1: ( 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 ) ; :: 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) )
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 A1, Def1; :: thesis: verum

end;

then consider q being POINT of IPP such that
A2: ( q on O & not q on B & not q on Q ) and
A3: (IncProj C,a,A) * (IncProj B,b,C) = (IncProj Q,a,A) * (IncProj B,q,Q) by A1, 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 A2; :: thesis: (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q)
A4: ( IncProj B,q,Q is one-to-one & IncProj Q,a,A is one-to-one ) by A1, A2, Th8;
A5: ( IncProj B,b,C is one-to-one & IncProj C,a,A is one-to-one ) by A1, Th8;
thus (IncProj C,b,B) * (IncProj A,a,C) = ((IncProj B,b,C) " ) * (IncProj A,a,C) by A1, Th9
.= ((IncProj B,b,C) " ) * ((IncProj C,a,A) " ) by A1, Th9
.= ((IncProj Q,a,A) * (IncProj B,q,Q)) " by A3, A5, FUNCT_1:66
.= ((IncProj B,q,Q) " ) * ((IncProj Q,a,A) " ) by A4, FUNCT_1:66
.= (IncProj Q,q,B) * ((IncProj Q,a,A) " ) by A2, Th9
.= (IncProj Q,q,B) * (IncProj A,a,Q) by A1, Th9 ; :: thesis: verum