let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, c, d, p, pp9, q being POINT of IPP
for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds
( q <> a & q <> b & not q on A & not q on Q )
let a, b, c, d, p, pp9, q be POINT of IPP; :: thesis: for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds
( q <> a & q <> b & not q on A & not q on Q )
let O1, O2, O3, A, B, C, O, Q be LINE of IPP; :: thesis: ( not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 implies ( q <> a & q <> b & not q on A & not q on Q ) )
assume that
A1: not a on A and
A2: not a on C and
A3: not b on C and
A4: not b on Q and
A5: not A,B,C are_concurrent and
A6: not B,C,O are_concurrent and
A7: A <> Q and
A8: Q <> C and
A9: a <> b and
A10: {c,p} on A and
A11: d on B and
A12: {c,d} on C and
A13: {a,b,q} on O and
A14: {c,pp9} on Q and
A15: {a,d,p} on O1 and
A16: {q,p,pp9} on O2 and
A17: {b,d,pp9} on O3 ; :: thesis: ( q <> a & q <> b & not q on A & not q on Q )
A18: d on C by A12, INCSP_1:1;
A19: c on C by A12, INCSP_1:1;
A20: c on A by A10, INCSP_1:1;
then A21: c <> d by A5, A11, A19;
A22: d on O1 by A15, INCSP_1:2;
A23: pp9 on Q by A14, INCSP_1:1;
A24: pp9 on O3 by A17, INCSP_1:2;
A25: pp9 on O2 by A16, INCSP_1:2;
A26: a on O1 by A15, INCSP_1:2;
A27: b on O3 by A17, INCSP_1:2;
A28: d on O3 by A17, INCSP_1:2;
A29: q on O by A13, INCSP_1:2;
A30: b on O by A13, INCSP_1:2;
A31: q <> pp9

proof

assume not q <> pp9 ; :: thesis: contradiction
then O3 = O by A4, A30, A29, A27, A24, A23, INCPROJ:def 4;
hence contradiction by A6, A11, A18, A28; :: thesis: verum

end;

A32: ( pp9 on O2 & q on O2 ) by A16, INCSP_1:2;
A33: ( pp9 on Q & p on O2 ) by A14, A16, INCSP_1:1, INCSP_1:2;
A34: p on A by A10, INCSP_1:1;
A35: c on Q by A14, INCSP_1:1;
then A36: pp9 <> d by A8, A19, A18, A23, A21, INCPROJ:def 4;
A37: O1 <> O2

proof

assume not O1 <> O2 ; :: thesis: contradiction
then A38: a on O3 by A26, A22, A25, A28, A24, A36, INCPROJ:def 4;
( a on O & b on O ) by A13, INCSP_1:2;
then d on O by A9, A28, A27, A38, INCPROJ:def 4;
hence contradiction by A6, A11, A18; :: thesis: verum

end;

A39: p on O1 by A15, INCSP_1:2;
then A40: p <> c by A2, A19, A18, A26, A22, A21, INCPROJ:def 4;
A41: not q on Q

proof

assume q on Q ; :: thesis: contradiction
then p on Q by A33, A32, A31, INCPROJ:def 4;
hence contradiction by A7, A20, A35, A34, A40, INCPROJ:def 4; :: thesis: verum

end;

A42: a on O by A13, INCSP_1:2;
A43: q <> p

proof

assume not q <> p ; :: thesis: contradiction
then O = O1 by A1, A42, A26, A34, A39, A29, INCPROJ:def 4;
hence contradiction by A6, A11, A18, A22; :: thesis: verum

end;

A44: p on O2 by A16, INCSP_1:2;
pp9 <> c by A3, A19, A18, A28, A27, A24, A21, INCPROJ:def 4;
then A45: A <> O2 by A7, A20, A35, A25, A23, INCPROJ:def 4;
A46: q on O2 by A16, INCSP_1:2;
A47: p <> d by A5, A11, A18, A34;
q <> b

proof

assume not q <> b ; :: thesis: contradiction
then O2 = O3 by A4, A46, A25, A27, A24, A23, INCPROJ:def 4;
hence contradiction by A22, A39, A44, A28, A47, A37, INCPROJ:def 4; :: thesis: verum

end;

hence ( q <> a & q <> b & not q on A & not q on Q ) by A26, A34, A39, A46, A44, A45, A37, A43, A41, INCPROJ:def 4; :: thesis: verum