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 that
A1: ( not p on K & not p on L ) and
A2: y in rng (IncProj (K,p,L)) ; :: thesis: y on L
consider x being POINT of IPP such that
A3: x in dom (IncProj (K,p,L)) and
A4: y = (IncProj (K,p,L)) . x by A2, PARTFUN1:3;
x on K by A1, A3, Def1;
hence y on L by A1, A4, Th20; :: thesis: verum