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