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 A & q <> b & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,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 A & q <> b & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,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 A & q <> b & not A,B,C are_concurrent implies ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) )
consider c being POINT of IPP such that
A1: ( c on A & c on C ) by INCPROJ:def 14;
assume A2: ( 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 A & q <> b & not A,B,C are_concurrent ) ; :: thesis: ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )

A3: now

assume B,C,O are_concurrent ; :: thesis: ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
then consider Q being LINE of IPP such that
A4: c on Q and
A5: ( not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A2, A1, Lm4;
take Q = Q; :: thesis: ( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
thus A,C,Q are_concurrent by A1, A4, Def1; :: thesis: ( not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
thus ( not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A5; :: thesis: verum

end;

now

assume not B,C,O are_concurrent ; :: thesis: ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
then consider Q being LINE of IPP such that
A6: c on Q and
A7: ( not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A2, A1, Lm3;
take Q = Q; :: thesis: ( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
thus A,C,Q are_concurrent by A1, A6, Def1; :: thesis: ( not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )
thus ( not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A7; :: thesis: verum

end;

hence ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) ) by A3; :: thesis: verum