let IPP be 2-dimensional Desarguesian IncProjSp; 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; 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; ( 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
; for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x
let x be POINT of IPP; ( x on K implies (IncProj (K,p,K)) . x = x )
A2:
ex X being LINE of IPP st
( p on X & x on X )
by INCPROJ:def 5;
assume
x on K
; (IncProj (K,p,K)) . x = x
hence
(IncProj (K,p,K)) . x = x
by A1, A2, Def1; verum