let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for p, x, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds
y on L
let p, x, y be POINT of IPP; :: thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds
y on L
let K, L be LINE of IPP; :: thesis: ( not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x implies y on L )
assume A1: ( not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x ) ; :: thesis: y on L
consider X being LINE of IPP such that
A2: ( p on X & x on X ) by INCPROJ:def 5;
ex z being POINT of IPP st
( z on L & z on X ) by INCPROJ:def 9;
hence y on L by A1, A2, Def1; :: thesis: verum