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 that
A1: not p on K and
A2: not p on L and
A3: a1 on K and
A4: b1 on K and
A5: (IncProj (K,p,L)) . a1 = a2 and
A6: (IncProj (K,p,L)) . b1 = b2 and
A7: a2 = b2 ; :: thesis: a1 = b1
reconsider a2 = (IncProj (K,p,L)) . a1 as POINT of IPP by A5;
A8: a2 on L by A1, A2, A3, Th20;
then consider A being LINE of IPP such that
A9: p on A and
A10: a1 on A and
A11: a2 on A by A1, A2, A3, Def1;
reconsider b2 = (IncProj (K,p,L)) . b1 as Element of the Points of IPP by A6;
b2 on L by A1, A2, A4, Th20;
then consider B being LINE of IPP such that
A12: p on B and
A13: b1 on B and
A14: b2 on B by A1, A2, A4, Def1;
A = B by A2, A5, A6, A7, A8, A9, A11, A12, A14, INCPROJ:def 4;
hence a1 = b1 by A1, A3, A4, A9, A10, A13, INCPROJ:def 4; :: thesis: verum