let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: 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 holds
(IncProj (K,p,L)) . x is POINT of IPP
let p, x be POINT of IPP; :: thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K holds
(IncProj (K,p,L)) . x is POINT of IPP
let K, L be LINE of IPP; :: thesis: ( not p on K & not p on L & x on K implies (IncProj (K,p,L)) . x is POINT of IPP )
assume ( not p on K & not p on L & x on K ) ; :: thesis: (IncProj (K,p,L)) . x is POINT of IPP
then x in dom (IncProj (K,p,L)) by Def1;
hence (IncProj (K,p,L)) . x is POINT of IPP by PARTFUN1:4; :: thesis: verum