let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: 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 )
let o1, o2 be POINT of IPP; :: thesis: 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 )
let O1, O2, O3 be LINE of IPP; :: thesis: ( not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1 <> O3 implies 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 ) )
assume that
A1: ( not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 ) and
A2: O1,O2,O3 are_concurrent and
A3: O1 <> O3 ; :: thesis: 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 )
ex p being POINT of IPP st
( p on O1 & p on O2 & p on O3 ) by A2, Def1;
hence 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 A1, A3, PROJRED1:28; :: thesis: verum