theorem
for
IPP being
2-dimensional Desarguesian IncProjSp for
c,
p,
q being
POINT of
IPP for
K,
L,
R being
LINE of
IPP st not
p on K & not
p on L & not
q on L & not
q on R &
c on K &
c on L &
c on R &
K <> R holds
ex
o being
POINT of
IPP st
( not
o on K & not
o on R &
(IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (
K,
o,
R) )