theorem Th31: :: COMBGRAS:31

for k being Nat
for X being non empty set st 0 < k & k + 3 c= card X holds
for F being IncProjMap over G_ ((k + 1),X), G_ ((k + 1),X) st F is automorphism holds
ex H being IncProjMap over G_ (k,X), G_ (k,X) st
( H is automorphism & the line-map of H = the point-map of F & ( for A being POINT of (G_ (k,X))
for B being finite set st B = A holds
H . A = meet (F .: (^^ (B,X,(k + 1)))) ) )