let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, c, d, q, o, o9, o99, oo9 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds
( not q on A & not q on Q & b <> q )

let a, b, c, d, q, o, o9, o99, oo9 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds
( not q on A & not q on Q & b <> 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O implies ( not q on A & not q on Q & b <> q ) )
assume that
A1: not a on A and
A2: not a on C and
A3: not b on B and
A4: not b on C and
A5: not b on Q and
A6: not A,B,C are_concurrent and
A7: a <> b and
A8: A <> Q and
A9: {c,o} on A and
A10: {o,o99,d} on B and
A11: {c,d,o9} on C and
A12: {a,b,d} on O and
A13: {c,oo9} on Q and
A14: {a,o,o9} on O1 and
A15: {b,o9,oo9} on O2 and
A16: {o,oo9,q} on O3 and
A17: q on O ; :: thesis: ( not q on A & not q on Q & b <> q )
A18: o on B by ;
A19: ( c on A & c on Q ) by ;
A20: o on A by ;
A21: oo9 on O2 by ;
A22: ( b on O2 & oo9 on O2 ) by ;
A23: oo9 on Q by ;
A24: b on O2 by ;
A25: o on O1 by ;
A26: o on A by ;
A27: d on C by ;
then A28: o <> d by A6, A26, A18;
A29: d on B by ;
A30: b on O by ;
A31: oo9 on Q by ;
A32: o9 on O2 by ;
A33: q on O3 by ;
A34: a on O1 by ;
A35: d on O by ;
A36: a on O by ;
A37: O1 <> O2
proof
assume not O1 <> O2 ; :: thesis: contradiction
then o on O by ;
hence contradiction by A3, A18, A29, A30, A35, A28, INCPROJ:def 4; :: thesis: verum
end;
A38: ( o on O3 & oo9 on O3 ) by ;
A39: o9 on C by ;
then A40: o <> o9 by A6, A26, A18;
A41: b <> q
proof
assume not b <> q ; :: thesis: contradiction
then A42: o on O2 by ;
A43: o9 on O2 by ;
( o on O1 & o9 on O1 ) by ;
hence contradiction by A37, A40, A42, A43, INCPROJ:def 4; :: thesis: verum
end;
A44: c on A by ;
A45: c on C by ;
then A46: o <> c by A6, A44, A18;
A47: o9 on O1 by ;
then o9 <> c by ;
then A48: c <> oo9 by ;
o9 <> d
proof end;
then O <> O2 by ;
then A49: q <> oo9 by ;
A50: c on Q by ;
A51: not q on Q
proof
assume q on Q ; :: thesis: contradiction
then o on Q by ;
hence contradiction by A8, A44, A26, A50, A46, INCPROJ:def 4; :: thesis: verum
end;
A52: q <> o by ;
not q on A
proof
assume q on A ; :: thesis: contradiction
then oo9 on A by ;
hence contradiction by A8, A19, A23, A48, INCPROJ:def 4; :: thesis: verum
end;
hence ( not q on A & not q on Q & b <> q ) by ; :: thesis: verum