let IPP be 2-dimensional Desarguesian IncProjSp; 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; 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; ( 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 )
; 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; verum