for k being Nat
for X being non empty set st 0 < k & k + 1 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) holds
( F is automorphism iff ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )