for P1, P2 being IncProjStr st 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 #) holds
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 ;