theorem Th19:
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 )