for S1, S2 being IncProjStr
for F1, F2 being IncProjMap over S1,S2 st IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #) & F1 is incidence_preserving holds
F2 is incidence_preserving