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 ) )
consider X being LINE of IPP such that
A1: ( o on X & y on X ) by INCPROJ:def 5;
consider x being POINT of IPP such that
A2: x on X and
A3: x on A by INCPROJ:def 9;
assume ( 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 )
then (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