let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for p being POINT of IPP
for K, L being LINE of IPP
for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj K,p,L) . a1 = a2 & (IncProj K,p,L) . b1 = b2 & a2 = b2 holds
a1 = b1
let p be POINT of IPP; :: thesis: for K, L being LINE of IPP
for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj K,p,L) . a1 = a2 & (IncProj K,p,L) . b1 = b2 & a2 = b2 holds
a1 = b1
let K, L be LINE of IPP; :: thesis: for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj K,p,L) . a1 = a2 & (IncProj K,p,L) . b1 = b2 & a2 = b2 holds
a1 = b1
let a1, b1, a2, b2 be POINT of IPP; :: thesis: ( not p on K & not p on L & a1 on K & b1 on K & (IncProj K,p,L) . a1 = a2 & (IncProj K,p,L) . b1 = b2 & a2 = b2 implies a1 = b1 )
assume A1: ( not p on K & not p on L & a1 on K & b1 on K & (IncProj K,p,L) . a1 = a2 & (IncProj K,p,L) . b1 = b2 & a2 = b2 ) ; :: thesis: a1 = b1
then reconsider a2 = (IncProj K,p,L) . a1 as POINT of IPP ;
A2: a2 on L by A1, Th23;
then consider A being LINE of IPP such that
A3: ( p on A & a1 on A & a2 on A ) by A1, Def1;
reconsider b2 = (IncProj K,p,L) . b1 as Element of the Points of IPP by A1;
b2 on L by A1, Th23;
then consider B being LINE of IPP such that
A4: ( p on B & b1 on B & b2 on B ) by A1, Def1;
A = B by A1, A2, A3, A4, INCPROJ:def 9;
hence a1 = b1 by A1, A3, A4, INCPROJ:def 9; :: thesis: verum