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