theorem Th19: :: PROJRED2:19
for IPP being 2-dimensional Desarguesian IncProjSp
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 q on A & not A,B,C are_concurrent & a <> b & b <> 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 b on Q & not q on Q & A <> Q )