let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for p, y being POINT of
for K, L being LINE of st not p on K & not p on L & y in rng (IncProj K,p,L) holds
y on L
let p, y be POINT of ; :: thesis: for K, L being LINE of st not p on K & not p on L & y in rng (IncProj K,p,L) holds
y on L
let K, L be LINE of ; :: thesis: ( not p on K & not p on L & y in rng (IncProj K,p,L) implies y on L )
assume that
A1: ( not p on K & not p on L ) and
A2: y in rng (IncProj K,p,L) ; :: thesis: y on L
consider x being POINT of such that
A3: x in dom (IncProj K,p,L) and
A4: y = (IncProj K,p,L) . x by A2, PARTFUN1:26;
x on K by A1, A3, Def1;
hence y on L by A1, A4, Th23; :: thesis: verum