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

proof

assume not O1 <> O2 ; :: thesis: contradiction
then o on O by A2, INCPROJ:def 9;
hence contradiction by A2, A11, INCPROJ:def 9; :: thesis: verum

end;

A13: q <> o by A2, A11, INCPROJ:def 9;
A14: c <> oo' by A2, A10, INCPROJ:def 9;
A15: not q on A

proof

assume q on A ; :: thesis: contradiction
then oo' on A by A4, A7, A8, A13, INCPROJ:def 9;
hence contradiction by A1, A3, A6, A14, INCPROJ:def 9; :: thesis: verum

end;

o' <> d

proof

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

end;

then O <> O2 by A2, INCPROJ:def 9;
then A16: q <> oo' by A2, INCPROJ:def 9;
A17: not q on Q

proof

assume q on Q ; :: thesis: contradiction
then o on Q by A6, A7, A8, A16, INCPROJ:def 9;
hence contradiction by A2, A9, INCPROJ:def 9; :: thesis: verum

end;

A18: o <> o' by A2, Def1;
b <> q

proof

assume not b <> q ; :: thesis: contradiction
then ( o on O1 & o' on O1 & o on O2 & o' on O2 ) by A1, A5, A6, A7, A8, INCPROJ:def 9, INCSP_1:12;
hence contradiction by A12, A18, INCPROJ:def 9; :: thesis: verum

end;

hence ( not q on A & not q on Q & b <> q ) by A15, A17; :: thesis: verum