theorem Th25: :: COMBGRAS:25

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