let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, q, c, o, o'', d, o', oo' 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 & a <> b & b <> q & {c,o} on A & {o,o'',d} on B & {c,d,o'} on C & {a,b,d} on O & {c,oo'} on Q & {a,o,o'} on O1 & {b,o',oo'} on O2 & {o,oo',q} on O3 & q on O holds
( not b on Q & not q on Q & A <> Q )
let a, b, q, c, o, o'', d, o', oo' 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 & a <> b & b <> q & {c,o} on A & {o,o'',d} on B & {c,d,o'} on C & {a,b,d} on O & {c,oo'} on Q & {a,o,o'} on O1 & {b,o',oo'} on O2 & {o,oo',q} on O3 & q on O holds
( not b on Q & not q on Q & A <> 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 & a <> b & b <> q & {c,o} on A & {o,o'',d} on B & {c,d,o'} on C & {a,b,d} on O & {c,oo'} on Q & {a,o,o'} on O1 & {b,o',oo'} on O2 & {o,oo',q} on O3 & q on O implies ( not b on Q & not q on Q & A <> 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 & a <> b & b <> q & {c,o} on A & {o,o'',d} on B & {c,d,o'} on C & {a,b,d} on O & {c,oo'} on Q & {a,o,o'} on O1 & {b,o',oo'} on O2 & {o,oo',q} on O3 & q on O ) ; :: thesis: ( not b on Q & not q on Q & A <> Q )
then A2: ( 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 & a <> b & b <> q & c on A & o on A & o on B & o'' on B & d on B & c on C & d on C & o' on C & a on O & b on O & d on O & c on Q & oo' on Q & a on O1 & o on O1 & o' on O1 & b on O2 & o' on O2 & oo' on O2 & o on O3 & oo' on O3 & q on O3 & q on O ) by INCSP_1:11, INCSP_1:12;
A3: ( c on A & c on C & c on Q ) by A1, INCSP_1:11, INCSP_1:12;
A4: ( d on B & d on C & d on O ) by A1, INCSP_1:12;
A5: ( o on A & o on B ) by A1, INCSP_1:11, INCSP_1:12;
A6: ( b on O2 & o' on O2 ) by A1, INCSP_1:12;
A7: ( oo' on Q & oo' on O2 ) by A1, INCSP_1:11, INCSP_1:12;
A8: ( o on O3 & oo' on O3 ) by A1, INCSP_1:12;
A9: ( q on O3 & q on O ) by A1, INCSP_1:12;
A10: o <> c by A2, Def1;
then A11: o' <> c by A2, INCPROJ:def 9;
A12: o <> d by A2, Def1;
A13: ( C <> O1 & C <> O2 ) by A1, INCSP_1:12;
A14: O1 <> O2

proof

assume not O1 <> O2 ; :: thesis: contradiction
then o on O by A2, INCPROJ:def 9;
then O = B by A4, A5, A12, INCPROJ:def 9;
hence contradiction by A1, INCSP_1:12; :: thesis: verum

end;

o' <> d

proof

assume not o' <> d ; :: thesis: contradiction
then O1 = O by A2, INCPROJ:def 9;
hence contradiction by A2, A12, INCPROJ:def 9; :: thesis: verum

end;

then A15: O <> O2 by A2, INCPROJ:def 9;
o <> o' by A2, Def1;
then A16: o <> oo' by A2, A14, INCPROJ:def 9;
A17: b <> oo'

proof

assume not b <> oo' ; :: thesis: contradiction
then ( b on O3 & q on O3 & b on O & q on O & b <> q ) by A1, INCSP_1:12;
then o on O by A8, INCPROJ:def 9;
then O = B by A4, A5, A12, INCPROJ:def 9;
hence contradiction by A1, INCSP_1:12; :: thesis: verum

end;

A18: not b on Q

proof

assume b on Q ; :: thesis: contradiction
then ( o' on C & c on C & o' on O2 & c on O2 ) by A1, A3, A6, A7, A17, INCPROJ:def 9, INCSP_1:12;
hence contradiction by A11, A13, INCPROJ:def 9; :: thesis: verum

end;

A19: q <> oo' by A2, A15, INCPROJ:def 9;
not q on Q

proof

assume q on Q ; :: thesis: contradiction
then Q = O3 by A7, A8, A9, A19, INCPROJ:def 9;
hence contradiction by A2, A10, INCPROJ:def 9; :: thesis: verum

end;

hence ( not b on Q & not q on Q & A <> Q ) by A2, A16, A18, INCPROJ:def 9; :: thesis: verum