:: deftheorem defines incidence_preserving COMBGRAS:def 8 :
for S1, S2 being IncProjStr
for F being IncProjMap over S1,S2 holds
( F is incidence_preserving iff for A1 being POINT of S1
for L1 being LINE of S1 holds
( A1 on L1 iff F . A1 on F . L1 ) );