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