theorem :: PROJRED2:13

for IPP being 2-dimensional Desarguesian IncProjSp
for o1, o2 being POINT of IPP
for O1, O2, O3 being LINE of IPP st not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1 <> O3 holds
ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) ) by PROJRED1:25;