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

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