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) )