:: deftheorem defines automorphism COMBGRAS:def 9 :
for S being IncProjStr
for F being IncProjMap over S,S holds
( F is automorphism iff ( the line-map of F is bijective & the point-map of F is bijective & F is incidence_preserving ) );