let IPP be 2-dimensional Desarguesian IncProjSp; 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; 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; 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; ( 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
; 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; verum