let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, q, c, p, d, pp' being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & not B,C,O are_concurrent & a <> b & b <> q & q <> a & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp'} on Q & {a,d,p} on O1 & {q,p,pp'} on O2 & {b,d,pp'} on O3 holds
( Q <> A & Q <> C & not q on Q & not b on Q )
let a, b, q, c, p, d, pp' be POINT of IPP; :: thesis: for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & not B,C,O are_concurrent & a <> b & b <> q & q <> a & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp'} on Q & {a,d,p} on O1 & {q,p,pp'} on O2 & {b,d,pp'} on O3 holds
( Q <> A & Q <> C & not q on Q & not b on Q )
let A, C, B, O, Q, O1, O2, O3 be LINE of IPP; :: thesis: ( not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & not B,C,O are_concurrent & a <> b & b <> q & q <> a & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp'} on Q & {a,d,p} on O1 & {q,p,pp'} on O2 & {b,d,pp'} on O3 implies ( Q <> A & Q <> C & not q on Q & not b on Q ) )
assume A1: ( not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & not B,C,O are_concurrent & a <> b & b <> q & q <> a & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp'} on Q & {a,d,p} on O1 & {q,p,pp'} on O2 & {b,d,pp'} on O3 ) ; :: thesis: ( Q <> A & Q <> C & not q on Q & not b on Q )
then A2: ( not a on A & not b on B & not a on C & not b on C & not q on A & not A,B,C are_concurrent & c on A & c on C & c on Q & a <> b & q <> a & q <> b & a on O & b on O & not B,C,O are_concurrent & d on C & d on B & a on O1 & d on O1 & p on A & p on O1 & q on O & q on O2 & p on O2 & pp' on O2 & d on O3 & b on O3 & pp' on O3 & pp' on Q ) by INCSP_1:11, INCSP_1:12;
A3: ( p on O2 & pp' on O2 ) by A1, INCSP_1:12;
A4: c <> d by A2, Def1;
then A5: p <> c by A2, INCPROJ:def 9;
A6: p <> d by A2, Def1;
A7: ( O <> O1 & O <> O3 ) by A2, Def1;
A8: p <> pp'

proof

assume not p <> pp' ; :: thesis: contradiction
then O1 = O3 by A2, A6, INCPROJ:def 9;
hence contradiction by A2, A7, INCPROJ:def 9; :: thesis: verum

end;

A9: pp' <> d

proof

assume not pp' <> d ; :: thesis: contradiction
then ( a on O & q on O & a on O1 & q on O1 & a <> q ) by A2, A6, INCPROJ:def 9;
hence contradiction by A7, INCPROJ:def 9; :: thesis: verum

end;

A10: O3 <> Q by A2, A4, INCPROJ:def 9;
A11: O2 <> Q by A2, A5, INCPROJ:def 9;
A12: not b on Q

proof

assume b on Q ; :: thesis: contradiction
then ( b on O2 & q on O2 & b on O & q on O & b <> q ) by A2, A10, INCPROJ:def 9;
then p on O by A3, INCPROJ:def 9;
hence contradiction by A2, A7, INCPROJ:def 9; :: thesis: verum

end;

not q on Q

proof

assume q on Q ; :: thesis: contradiction
then q = pp' by A2, A11, INCPROJ:def 9;
hence contradiction by A2, A7, INCPROJ:def 9; :: thesis: verum

end;

hence ( Q <> A & Q <> C & not q on Q & not b on Q ) by A2, A8, A9, A12, INCPROJ:def 9; :: thesis: verum