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