let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for p, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj K,p,L) holds
y on L
let p, y be POINT of IPP; :: thesis: for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj K,p,L) holds
y on L
let K, L be LINE of IPP; :: thesis: ( not p on K & not p on L & y in rng (IncProj K,p,L) implies y on L )
assume A1: ( not p on K & not p on L & y in rng (IncProj K,p,L) ) ; :: thesis: y on L
then consider x being POINT of IPP such that
A2: ( x in dom (IncProj K,p,L) & y = (IncProj K,p,L) . x ) by PARTFUN1:26;
x on K by A1, A2, Def1;
hence y on L by A1, A2, Th23; :: thesis: verum