theorem Th24: :: COMBGRAS:24

for k being Nat
for X being non empty set st k = 1 & k + 1 c= card X 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)