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