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 ;
A19: c on C by ;
A20: c on A by ;
then A21: c <> d by A5, A11, A19;
A22: d on O1 by ;
A23: pp9 on Q by ;
A24: pp9 on O3 by ;
A25: pp9 on O2 by ;
A26: a on O1 by ;
A27: b on O3 by ;
A28: d on O3 by ;
A29: q on O by ;
A30: b on O by ;
A31: q <> pp9
proof
assume not q <> pp9 ; :: thesis: contradiction
then O3 = O by ;
hence contradiction by A6, A11, A18, A28; :: thesis: verum
end;
A32: ( pp9 on O2 & q on O2 ) by ;
A33: ( pp9 on Q & p on O2 ) by ;
A34: p on A by ;
A35: c on Q by ;
then A36: pp9 <> d by ;
A37: O1 <> O2
proof
assume not O1 <> O2 ; :: thesis: contradiction
then A38: a on O3 by ;
( a on O & b on O ) by ;
then d on O by ;
hence contradiction by A6, A11, A18; :: thesis: verum
end;
A39: p on O1 by ;
then A40: p <> c by ;
A41: not q on Q
proof
assume q on Q ; :: thesis: contradiction
then p on Q by ;
hence contradiction by A7, A20, A35, A34, A40, INCPROJ:def 4; :: thesis: verum
end;
A42: a on O by ;
A43: q <> p
proof
assume not q <> p ; :: thesis: contradiction
then O = O1 by ;
hence contradiction by A6, A11, A18, A22; :: thesis: verum
end;
A44: p on O2 by ;
pp9 <> c by ;
then A45: A <> O2 by ;
A46: q on O2 by ;
A47: p <> d by A5, A11, A18, A34;
q <> b
proof
assume not q <> b ; :: thesis: contradiction
then O2 = O3 by ;
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 ; :: thesis: verum