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 & x on L holds
(IncProj K,p,L) . x = x
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 & x on L holds
(IncProj K,p,L) . x = x
let K, L be LINE of IPP; :: thesis: ( not p on K & not p on L & x on K & x on L implies (IncProj K,p,L) . x = x )
A1: ex A being LINE of IPP st
( p on A & x on A ) by INCPROJ:def 10;
assume ( not p on K & not p on L & x on K & x on L ) ; :: thesis: (IncProj K,p,L) . x = x
hence (IncProj K,p,L) . x = x by A1, Def1; :: thesis: verum