let P1, P2 be IncProjStr ; :: thesis: ( IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) implies for A1 being POINT of P1
for A2 being POINT of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2 )
assume A1: IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) ; :: thesis: for A1 being POINT of P1
for A2 being POINT of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let A1 be POINT of P1; :: thesis: for A2 being POINT of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let A2 be POINT of P2; :: thesis: ( A1 = A2 implies for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2 )
assume A2: A1 = A2 ; :: thesis: for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let L1 be LINE of P1; :: thesis: for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let L2 be LINE of P2; :: thesis: ( L1 = L2 & A1 on L1 implies A2 on L2 )
assume ( L1 = L2 & A1 on L1 ) ; :: thesis: A2 on L2
then [A2,L2] in the Inc of P2 by A1, A2, INCSP_1:def 1;
hence A2 on L2 by INCSP_1:def 1; :: thesis: verum