let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for o, y being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B & y on B holds
ex x being POINT of IPP st
( x on A & (IncProj A,o,B) . x = y )
let o, y be POINT of IPP; :: thesis: for A, B being LINE of IPP st not o on A & not o on B & y on B holds
ex x being POINT of IPP st
( x on A & (IncProj A,o,B) . x = y )
let A, B be LINE of IPP; :: thesis: ( not o on A & not o on B & y on B implies ex x being POINT of IPP st
( x on A & (IncProj A,o,B) . x = y ) )
assume A1: ( not o on A & not o on B & y on B ) ; :: thesis: ex x being POINT of IPP st
( x on A & (IncProj A,o,B) . x = y )
consider X being LINE of IPP such that
A2: ( o on X & y on X ) by INCPROJ:def 10;
consider x being POINT of IPP such that
A3: ( x on X & x on A ) by INCPROJ:def 14;
(IncProj A,o,B) . x = y by A1, A2, A3, PROJRED1:def 1;
hence ex x being POINT of IPP st
( x on A & (IncProj A,o,B) . x = y ) by A3; :: thesis: verum