let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on B & q <> a & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( B,C,Q are_concurrent & not a on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
let a, b, q be POINT of IPP; :: thesis: for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on B & q <> a & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( B,C,Q are_concurrent & not a on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
let A, B, C, O be LINE of IPP; :: thesis: ( not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on B & q <> a & not A,B,C are_concurrent implies ex Q being LINE of IPP st
( B,C,Q are_concurrent & not a on Q & 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: ( a <> b & a on O & b on O & q on O ) and
A6: not q on B and
A7: q <> a and
A8: not A,B,C are_concurrent ; :: thesis: ex Q being LINE of IPP st
( B,C,Q are_concurrent & not a on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
A9: ( IncProj C,a,A is one-to-one & IncProj B,b,C 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 A8, Def1; :: thesis: verum

end;

then consider Q being LINE of IPP such that
A10: B,C,Q are_concurrent and
A11: not a on Q and
A12: not q on Q and
A13: (IncProj C,a,A) * (IncProj B,b,C) = (IncProj Q,a,A) * (IncProj B,q,Q) by A1, A2, A3, A4, A5, A6, A7, Th24;
A14: ( IncProj Q,a,A is one-to-one & IncProj B,q,Q is one-to-one ) by A1, A6, A11, A12, Th8;
take Q ; :: thesis: ( B,C,Q are_concurrent & not a on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )
thus ( B,C,Q are_concurrent & not a on Q & not q on Q ) by A10, A11, A12; :: thesis: (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q)
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 A13, A9, FUNCT_1:66
.= ((IncProj B,q,Q) " ) * ((IncProj Q,a,A) " ) by A14, FUNCT_1:66
.= ((IncProj B,q,Q) " ) * (IncProj A,a,Q) by A1, A11, Th9
.= (IncProj Q,q,B) * (IncProj A,a,Q) by A6, A12, Th9 ; :: thesis: verum